# HG changeset patch
# User wenzelm
# Date 1169298563 -3600
# Node ID b9cbcd8be40ff1729c85755e9442b158a0cdd2e4
# Parent  8134eb5f45015e3bcc5980b54ccfa3d92973eee3
* ML within Isar: antiquotations;

diff -r 8134eb5f4501 -r b9cbcd8be40f NEWS
--- a/NEWS	Sat Jan 20 14:09:22 2007 +0100
+++ b/NEWS	Sat Jan 20 14:09:23 2007 +0100
@@ -750,6 +750,25 @@
 
 *** ML ***
 
+* ML within Isar: antiquotations allow to embed statically-checked
+formal entities in the source, referring to the context available at
+compile-time.  For example:
+
+ML {* @{typ "'a => 'b"} *}
+ML {* @{term "%x. x"} *}
+ML {* @{prop "x == y"} *}
+ML {* @{ctyp "'a => 'b"} *}
+ML {* @{cterm "%x. x"} *}
+ML {* @{cprop "x == y"} *}
+ML {* @{thm asm_rl} *}
+ML {* @{thms asm_rl} *}
+ML {* @{context} *}
+ML {* @{theory} *}
+ML {* @{theory Pure} *}
+ML {* @{simpset} *}
+ML {* @{claset} *}
+ML {* @{clasimpset} *}
+
 * Pure/library:
 
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list