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