1.1 --- a/ANNOUNCE	Tue Oct 02 16:06:41 2007 +0200
     1.2 +++ b/ANNOUNCE	Tue Oct 02 19:05:20 2007 +0200
     1.3 @@ -11,19 +11,22 @@
     1.4  
     1.5  The main highlights are:
     1.6  
     1.7 -* New 'function' package for general recursive function definitions.
     1.8 +* Fully featured support for nominal datatypes (binding structures)
     1.9 +due to the HOL-Nominal logic.
    1.10 +
    1.11 +* General local theory infrastructure for specifications depending on
    1.12 +parameters and assumptions (e.g. from locales, classes).
    1.13 +
    1.14 +* New basic specification elements 'definition', 'axiomatization',
    1.15 +'abbreviation', 'notation'.
    1.16  
    1.17  * New version of 'inductive' package for inductive predicates;
    1.18  separate variant 'inductive_set'.
    1.19  
    1.20 -* New basic specification elements 'definition', 'axiomatization',
    1.21 -'abbreviation', 'notation'.
    1.22 +* New 'function' package for general recursive function definitions.
    1.23  
    1.24  * New 'class' package combination of axclass + locale interpretation.
    1.25  
    1.26 -* Fully featured support for nominal datatypes (binding structures)
    1.27 -due to the HOL-Nominal logic.
    1.28 -
    1.29  * Various improvements in locale infrastructure (interpretation etc.)
    1.30  
    1.31  * Various improvements of Isar language elements and related proof
    1.32 @@ -32,9 +35,6 @@
    1.33  * Built-in Metis prover, external linkup for automated provers, and
    1.34  'sledghammer' command for automated proof synthesis.
    1.35  
    1.36 -* General local theory infrastructure for specifications depending on
    1.37 -parameters and assumptions (e.g. from locales, classes).
    1.38 -
    1.39  * Second generation code-generator for a subset of HOL, targeting SML,
    1.40  Haskell, and OCaml.
    1.41