diff -r 11996ea98bbe -r b3c6c9ef11b8 ANNOUNCE --- a/ANNOUNCE Sun Jan 20 13:59:13 2013 +0100 +++ b/ANNOUNCE Sun Jan 20 14:00:05 2013 +0100 @@ -1,40 +1,16 @@ -Subject: Announcing Isabelle2012 +Subject: Announcing Isabelle2013 To: isabelle-users@cl.cam.ac.uk -Isabelle2012 is now available. - -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. +Isabelle2013 is now available. -* 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. +This version consolidates Isabelle2012 and introduces numerous +improvements, see the NEWS file in the distribution for more details. +Some highlights are: -* 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. +* FIXME -You may get Isabelle2012 from the following mirror sites: +You may get Isabelle2013 from the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/