--- 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
+