# HG changeset patch
# User wenzelm
# Date 1295301248 -3600
# Node ID 313b0033034a51b41f1b0877f8c5af6f368a7a9c
# Parent  54a4512e29a67e678889cc7f3d4963b60c89818c
some announcement;

diff -r 54a4512e29a6 -r 313b0033034a ANNOUNCE
--- 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
 To: isabelle-users@cl.cam.ac.uk
 
-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
-are:
+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)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
   Munich (Germany)     http://isabelle.in.tum.de/