ML: improved antiquotations;

--- a/NEWS	Sat Jun 28 15:17:28 2008 +0200
+++ b/NEWS	Sat Jun 28 15:30:46 2008 +0200
@@ -67,6 +67,14 @@
 Syntax.read_term_global etc.; see also OldGoals.read_term as last
 resort for legacy applications.
 
+* Antiquotations: block-structured compilation context indicated by
+\<lbrace> ... \<rbrace>, and additional antiquotation forms:
+
+  @{let ?pat = term}
+  @{note name = fact}
+  @{thm name [attribs]}
+  @{thms name [attribs]}
+
 
 
 New in Isabelle2008 (June 2008)