# HG changeset patch
# User wenzelm
# Date 1214686586 -7200
# Node ID 7be8ff0611036df5d244522425bb8faf593ced87
# Parent  6c4649134fd6f19aa748e6ae93706e9bdff975db
tuned;

diff -r 6c4649134fd6 -r 7be8ff061103 NEWS
--- a/NEWS	Sat Jun 28 22:54:19 2008 +0200
+++ b/NEWS	Sat Jun 28 22:56:26 2008 +0200
@@ -22,7 +22,8 @@
 *** Document preparation ***
 
 * Antiquotation @{lemma} now imitates a regular terminal proof,
-demanding keyword 'by' and supporting the full method expressions.
+demanding keyword 'by' and supporting the full method expression
+syntax.
 
 
 *** HOL ***
@@ -76,12 +77,12 @@
 * Antiquotations: block-structured compilation context indicated by
 \<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
+  @{let ?pat = term}                    - term abbreviation (HO matching)
+  @{note name = fact}                   - fact abbreviation
+  @{thm fact}                           - singleton fact
+  @{thms fact}                          - general fact
+  @{lemma prop by method}               - singleton goal
+  @{lemma prop1 ... propN by method}    - general goal