diff -r 2ed7b34f58e6 -r f28efd37e18a ANNOUNCE
--- a/ANNOUNCE	Fri Nov 02 18:53:01 2007 +0100
+++ b/ANNOUNCE	Sun Nov 04 16:43:27 2007 +0100
@@ -7,9 +7,7 @@
 NEWS file in the distribution for more details.  Numerous existing
 concepts have been generalized and re-implemented based on novel
 system architecture.  New theories and proof tools have been added
-(mostly for HOL).
-
-The main highlights are:
+(mostly for HOL).  Some highlights are:
 
 * Support for nominal datatypes (binding structures) due to the
 HOL-Nominal logic.
@@ -33,16 +31,19 @@
 * Second generation code generator for a subset of HOL, targeting SML,
 Haskell, and OCaml.
 
-* Command 'normal_form' and method 'normalization'
-for evaluating terms with free variables.
+* Embedding of ML code into theories with static references to the
+logical context (via antiquotations).
 
-* Full list comprehension syntax.
+* Command 'normal_form' and method "normalization" for evaluating
+terms with free variables.
+
+* Full list comprehension syntax for HOL.
+
+* Much improved algebraic capabilities, including Groebner bases.
 
 * Parallel loading of theories based on native multicore support in
 Poly/ML 5.1.
 
-* Much improved algebraic capabilities, including Groebner bases.
-
 
 You may get Isabelle2007 from the following mirror sites: