diff -r 1e5f48e01e5e -r 59b54d80d2ae NEWS
--- a/NEWS	Thu Jul 10 11:17:16 2008 +0200
+++ b/NEWS	Thu Jul 10 13:37:31 2008 +0200
@@ -15,27 +15,28 @@
 
 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
 
-* New ML antiquotation 'code': takes constant as argument, generates
-corresponding code in background and inserts name of the corresponding resulting
-ML value/function/datatype constructor binding in place.  All occurences of 'code'
-with a single ML block are generated simultaneously.
-Provides a generic and safe interface for instrumentalizing code generation.
-See HOL/ex/Code_Antiq for a toy example, or HOL/Complex/ex/ReflectedFerrack
-for a more ambitious application.  In future you ought refrain from
-ad-hoc compiling generated SML code on the ML toplevel.
-Note that (for technical reasons) 'code' cannot refer to constants for which
-user-defined serializations are set.  Refer to the corresponding ML counterpart
+* New ML antiquotation @{code}: takes constant as argument, generates
+corresponding code in background and inserts name of the corresponding
+resulting ML value/function/datatype constructor binding in place.
+All occurrences of @{code} with a single ML block are generated
+simultaneously.  Provides a generic and safe interface for
+instrumentalizing code generation.  See HOL/ex/Code_Antiq for a toy
+example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious
+application.  In future you ought refrain from ad-hoc compiling
+generated SML code on the ML toplevel.  Note that (for technical
+reasons) @{code} cannot refer to constants for which user-defined
+serializations are set.  Refer to the corresponding ML counterpart
 directly in that cases.
 
 * Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
-interface instead. 
+interface instead.
 
 
 *** Document preparation ***
 
 * Antiquotation @{lemma} now imitates a regular terminal proof,
 demanding keyword 'by' and supporting the full method expression
-syntax.
+syntax just like the Isar command 'by'.
 
 
 *** HOL ***
@@ -106,13 +107,15 @@
 * Antiquotations: block-structured compilation context indicated by
 \<lbrace> ... \<rbrace>; additional antiquotation forms:
 
-  @{let ?pat = term}                    - term abbreviation (HO matching)
-  @{note name = fact}                   - fact abbreviation
-  @{thm fact}                           - singleton fact (with attributes)
-  @{thms fact}                          - general fact (with attributes)
-  @{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 (with attributes)
+  @{thms fact}                            - general fact (with attributes)
+  @{lemma prop by method}                 - singleton goal
+  @{lemma prop by meth1 meth2}            - singleton goal
+  @{lemma prop1 ... propN by method}      - general goal
+  @{lemma prop1 ... propN by meth1 meth2} - general goal
+  @{lemma (open) ...}                     - open derivation