# HG changeset patch
# User wenzelm
# Date 1214659846 -7200
# Node ID ca505e7b7591ba8d4099e482dd8986b517f0d961
# Parent  c706b72018262ade3fc0501d54f4f79647d620f3
ML: improved antiquotations;

diff -r c706b7201826 -r ca505e7b7591 NEWS
--- 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)