1.1 --- a/ANNOUNCE	Fri May 04 17:14:42 2012 +0200
     1.2 +++ b/ANNOUNCE	Sat May 05 18:21:55 2012 +0200
     1.3 @@ -3,10 +3,35 @@
     1.4  
     1.5  Isabelle2012 is now available.
     1.6  
     1.7 -This version significantly improves upon Isabelle2011-1, see the NEWS
     1.8 -file in the distribution for more details.  Some notable changes are:
     1.9 +This version introduces many changes and improvements over
    1.10 +Isabelle2011-1, see the NEWS file in the distribution for more
    1.11 +details.  Some highlights are:
    1.12  
    1.13 -* FIXME
    1.14 +* Improved Isabelle/jEdit Prover IDE (PIDE).
    1.15 +
    1.16 +* Support for block-structured specification contexts.
    1.17 +
    1.18 +* Discontinued old code generator.
    1.19 +
    1.20 +* Updated manuals: prog-prove, isar-ref, implementation, system.
    1.21 +
    1.22 +* HOL: type 'a set is proper type constructor again.
    1.23 +
    1.24 +* HOL: improved representation of numerals.
    1.25 +
    1.26 +* HOL: new transfer and lifting packages, improved quotient package.
    1.27 +
    1.28 +* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer.
    1.29 +
    1.30 +* HOL library enhancements, including HOL-Library and HOL-Probability.
    1.31 +
    1.32 +* HOL: more TPTP support.
    1.33 +
    1.34 +* Re-implementation of HOL-Import for HOL-Light.
    1.35 +
    1.36 +* ZF: some modernization of notation and proofs.
    1.37 +
    1.38 +* System integration: improved support of Windows platform.
    1.39  
    1.40  
    1.41  You may get Isabelle2012 from the following mirror sites: