diff -r 8c2e8cf22fad -r 74bc59c2c4a6 ANNOUNCE
--- 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.