From 2547b2324ec65075365606e536648d8cc203150c Mon Sep 17 00:00:00 2001
From: Makarius <makarius@sketis.net>
Date: Mon, 20 Dec 2021 16:27:16 +0100
Subject: [PATCH] Adhoc examples for ML antiquotations.

---
 NOTES.thy | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/NOTES.thy b/NOTES.thy
index f45aea38..32ab328f 100644
--- a/NOTES.thy
+++ b/NOTES.thy
@@ -253,6 +253,22 @@ text \<open>
     \<close>
 \<close>
 
+text \<open>Adhoc examples:\<close>
+
+ML \<open>
+  fun mk_plus x y = \<^Const>\<open>plus \<^Type>\<open>nat\<close> for x y\<close>;
+
+  fn \<^Const_>\<open>plus \<^Type>\<open>nat\<close> for \<^Const_>\<open>Groups.zero \<^Type>\<open>nat\<close>\<close> y\<close> => y;
+\<close>
+
+ML \<open>
+  fn (A, B) =>
+    \<^instantiate>\<open>A and B in term \<open>A \<and> B \<longrightarrow> B \<and> A\<close>\<close>;
+
+  fn (A, B) =>
+    \<^instantiate>\<open>A and B in lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by simp\<close>;
+\<close>
+
 end
 
 (* :maxLineLen=75: *)
\ No newline at end of file