# HG changeset patch
# User wenzelm
# Date 1336234915 -7200
# Node ID fa59eb662e6c0cd8d484bdb027b2321ad906cb16
# Parent  32c03d45fffe4c6a3577bcc8adfddb4c9397f7a7
some highlights of Isabelle2012;

diff -r 32c03d45fffe -r fa59eb662e6c ANNOUNCE
--- a/ANNOUNCE	Fri May 04 17:14:42 2012 +0200
+++ b/ANNOUNCE	Sat May 05 18:21:55 2012 +0200
@@ -3,10 +3,35 @@
 
 Isabelle2012 is now available.
 
-This version significantly improves upon Isabelle2011-1, see the NEWS
-file in the distribution for more details.  Some notable changes are:
+This version introduces many changes and improvements over
+Isabelle2011-1, see the NEWS file in the distribution for more
+details.  Some highlights are:
+
+* Improved Isabelle/jEdit Prover IDE (PIDE).
+
+* Support for block-structured specification contexts.
+
+* Discontinued old code generator.
+
+* Updated manuals: prog-prove, isar-ref, implementation, system.
+
+* HOL: type 'a set is proper type constructor again.
 
-* FIXME
+* HOL: improved representation of numerals.
+
+* HOL: new transfer and lifting packages, improved quotient package.
+
+* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer.
+
+* HOL library enhancements, including HOL-Library and HOL-Probability.
+
+* HOL: more TPTP support.
+
+* Re-implementation of HOL-Import for HOL-Light.
+
+* ZF: some modernization of notation and proofs.
+
+* System integration: improved support of Windows platform.
 
 
 You may get Isabelle2012 from the following mirror sites: