# HG changeset patch
# User wenzelm
# Date 1214686459 -7200
# Node ID 6c4649134fd6f19aa748e6ae93706e9bdff975db
# Parent  49a54b060457562a379ef73c380b75ba3d50b7f8
additional ML antiquotations;

diff -r 49a54b060457 -r 6c4649134fd6 NEWS
--- a/NEWS	Sat Jun 28 22:52:11 2008 +0200
+++ b/NEWS	Sat Jun 28 22:54:19 2008 +0200
@@ -74,12 +74,15 @@
 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]}
+\<lbrace> ... \<rbrace>; additional antiquotation forms:
+
+  @{let ?pat = term}			- term abbreviation
+  @{note name = fact}			- fact abbreviation
+  @{thm name [attribs]}			- singleton fact
+  @{thms name [attribs]}		- general fact
+  @{lemma prop by method}		- singleton goal
+  @{lemma prop1 ... propN by method}	- general goal
+