--- 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/
--- a/CONTRIBUTORS Sun Jan 20 13:59:13 2013 +0100
+++ b/CONTRIBUTORS Sun Jan 20 14:00:05 2013 +0100
@@ -18,7 +18,7 @@
including a smart type annotation algorithm and proof shrinking.
* December 2012: Alessandro Coglio, Kestrel
- Contributions to HOL's Lattice library
+ Contributions to HOL's Lattice library.
* November 2012: Fabian Immler, TUM
"Symbols" dockable for Isabelle/jEdit.
--- a/NEWS Sun Jan 20 13:59:13 2013 +0100
+++ b/NEWS Sun Jan 20 14:00:05 2013 +0100
@@ -379,7 +379,7 @@
with support for mixed, nested recursion and interesting non-free
datatypes.
-* HOL/Finite_Set and Relation: added new set and relation operations
+* HOL/Finite_Set and Relation: added new set and relation operations
expressed by Finite_Set.fold.
* New theory HOL/Library/RBT_Set: implementation of sets by red-black