1.1 --- a/ANNOUNCE	Fri Nov 02 18:53:01 2007 +0100
     1.2 +++ b/ANNOUNCE	Sun Nov 04 16:43:27 2007 +0100
     1.3 @@ -7,9 +7,7 @@
     1.4  NEWS file in the distribution for more details.  Numerous existing
     1.5  concepts have been generalized and re-implemented based on novel
     1.6  system architecture.  New theories and proof tools have been added
     1.7 -(mostly for HOL).
     1.8 -
     1.9 -The main highlights are:
    1.10 +(mostly for HOL).  Some highlights are:
    1.11  
    1.12  * Support for nominal datatypes (binding structures) due to the
    1.13  HOL-Nominal logic.
    1.14 @@ -33,16 +31,19 @@
    1.15  * Second generation code generator for a subset of HOL, targeting SML,
    1.16  Haskell, and OCaml.
    1.17  
    1.18 -* Command 'normal_form' and method 'normalization'
    1.19 -for evaluating terms with free variables.
    1.20 +* Embedding of ML code into theories with static references to the
    1.21 +logical context (via antiquotations).
    1.22  
    1.23 -* Full list comprehension syntax.
    1.24 +* Command 'normal_form' and method "normalization" for evaluating
    1.25 +terms with free variables.
    1.26 +
    1.27 +* Full list comprehension syntax for HOL.
    1.28 +
    1.29 +* Much improved algebraic capabilities, including Groebner bases.
    1.30  
    1.31  * Parallel loading of theories based on native multicore support in
    1.32  Poly/ML 5.1.
    1.33  
    1.34 -* Much improved algebraic capabilities, including Groebner bases.
    1.35 -
    1.36  
    1.37  You may get Isabelle2007 from the following mirror sites:
    1.38