some announcement;
Mon, 17 Jan 2011 22:54:08 +0100
changeset 41604 313b0033034a
parent 41603 54a4512e29a6
child 41605 7d035da21e9c
some announcement;
--- a/ANNOUNCE	Mon Jan 17 18:32:16 2011 +0100
+++ b/ANNOUNCE	Mon Jan 17 22:54:08 2011 +0100
@@ -1,34 +1,34 @@
-Subject: Announcing Isabelle2009-2
+Subject: Announcing Isabelle2011
-Isabelle2009-2 is now available.
+Isabelle2011 is now available.
-This release improves upon Isabelle2009-1 in many respects, see the
-NEWS file in the distribution for more details.  Some notable changes
+This version significantly improves upon Isabelle2009-2, see the NEWS
+file in the distribution for more details.  Some notable changes are:
-* Explicit proof terms for type class reasoning.
+* Experimental Prover IDE based on Isabelle/Scala and jEdit.
+* Coercive subtyping (configured in HOL/Complex_Main).
-* Robust treatment of concrete syntax for different logical entities;
-mixfix syntax in local proof context.
+* HOL code generation: Scala as another target language.
-* Type declarations and notation within local theory context.
+* HOL: partial_function definitions.
-* HOL: package for quotient types.
+* HOL: various tool enhancements, including Quickcheck, Nitpick,
+  Sledgehammer, SMT integration.
-* HOL code generation: simple concept for abstract datatypes obeying
-invariants (e.g. red-black trees).
+* HOL: various additions to theory library, including HOL-Algebra,
+  Imperative_HOL Multivariate_Analysis, Probability.
-* HOL: new development of the Reals using Cauchy Sequences.
-* HOL: reorganization of abstract algebra type class hierarchy.
+* HOLCF: reorganization of library and related tools.
-* HOL: substantial reorganization of main library and related tools.
+* HOL/SPARK: interactive proof environment for verification conditions
+  generated by the SPARK Ada program verifier.
-* HOLCF: reorganization of 'domain' package.
+* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
-You may get Isabelle2009-2 from the following mirror sites:
+You may get Isabelle2011 from the following mirror sites:
   Cambridge (UK)
   Munich (Germany)