1.1 --- a/ANNOUNCE	Fri Jun 04 16:55:08 2010 +0200
     1.2 +++ b/ANNOUNCE	Fri Jun 04 16:55:25 2010 +0200
     1.3 @@ -7,8 +7,25 @@
     1.4  NEWS file in the distribution for more details.  Some notable changes
     1.5  are:
     1.6  
     1.7 -* FIXME
     1.8 +* Explicit proof terms for type class reasoning.
     1.9  
    1.10 +* Authentic syntax for *all* logical entities (type classes, type
    1.11 +constructors, term constants): provides simple and robust
    1.12 +correspondence between formal entities and concrete syntax.
    1.13 +
    1.14 +* HOL: Package for constructing quotient types.
    1.15 +
    1.16 +* HOL: Code generation now with simple concept for abstract
    1.17 +datatypes obeying invariants;  applications for typical data structures
    1.18 +(e.g. search trees) can be found in the library.
    1.19 +
    1.20 +* HOL: New development of the Reals using Cauchy Sequences.
    1.21 +
    1.22 +* HOL: Reorganization of abstract algebra type class hierarchy.
    1.23 +
    1.24 +* Commands 'types', 'typedecl' and 'typedef' now work within a local theory
    1.25 +context -- without introducing dependencies on parameters or
    1.26 +assumptions.
    1.27  
    1.28  You may get Isabelle2009-2 from the following mirror sites:
    1.29  

     2.1 --- a/NEWS	Fri Jun 04 16:55:08 2010 +0200
     2.2 +++ b/NEWS	Fri Jun 04 16:55:25 2010 +0200
     2.3 @@ -139,6 +139,10 @@
     2.4  * Command 'defaultsort' has been renamed to 'default_sort', it works
     2.5  within a local theory context.  Minor INCOMPATIBILITY.
     2.6  
     2.7 +* Raw axioms/defs may no longer carry sort constraints, and raw defs
     2.8 +may no longer carry premises. User-level specifications are
     2.9 +transformed accordingly by Thm.add_axiom/add_def.
    2.10 +
    2.11  * Proof terms: Type substitutions on proof constants now use canonical
    2.12  order of type variables.  INCOMPATIBILITY for tools working with proof
    2.13  terms.