--- a/ANNOUNCE Tue Oct 02 16:06:41 2007 +0200
+++ b/ANNOUNCE Tue Oct 02 19:05:20 2007 +0200
@@ -11,19 +11,22 @@
The main highlights are:
-* New 'function' package for general recursive function definitions.
+* Fully featured support for nominal datatypes (binding structures)
+due to the HOL-Nominal logic.
+
+* General local theory infrastructure for specifications depending on
+parameters and assumptions (e.g. from locales, classes).
+
+* New basic specification elements 'definition', 'axiomatization',
+'abbreviation', 'notation'.
* New version of 'inductive' package for inductive predicates;
separate variant 'inductive_set'.
-* New basic specification elements 'definition', 'axiomatization',
-'abbreviation', 'notation'.
+* New 'function' package for general recursive function definitions.
* New 'class' package combination of axclass + locale interpretation.
-* Fully featured support for nominal datatypes (binding structures)
-due to the HOL-Nominal logic.
-
* Various improvements in locale infrastructure (interpretation etc.)
* Various improvements of Isar language elements and related proof
@@ -32,9 +35,6 @@
* Built-in Metis prover, external linkup for automated provers, and
'sledghammer' command for automated proof synthesis.
-* General local theory infrastructure for specifications depending on
-parameters and assumptions (e.g. from locales, classes).
-
* Second generation code-generator for a subset of HOL, targeting SML,
Haskell, and OCaml.