1.1 --- a/ANNOUNCE	Mon Jan 17 18:32:16 2011 +0100
     1.2 +++ b/ANNOUNCE	Mon Jan 17 22:54:08 2011 +0100
     1.3 @@ -1,34 +1,34 @@
     1.4 -Subject: Announcing Isabelle2009-2
     1.5 +Subject: Announcing Isabelle2011
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2009-2 is now available.
     1.9 +Isabelle2011 is now available.
    1.10  
    1.11 -This release improves upon Isabelle2009-1 in many respects, see the
    1.12 -NEWS file in the distribution for more details.  Some notable changes
    1.13 -are:
    1.14 +This version significantly improves upon Isabelle2009-2, see the NEWS
    1.15 +file in the distribution for more details.  Some notable changes are:
    1.16  
    1.17 -* Explicit proof terms for type class reasoning.
    1.18 +* Experimental Prover IDE based on Isabelle/Scala and jEdit.
    1.19  
    1.20 -* Robust treatment of concrete syntax for different logical entities;
    1.21 -mixfix syntax in local proof context.
    1.22 +* Coercive subtyping (configured in HOL/Complex_Main).
    1.23  
    1.24 -* Type declarations and notation within local theory context.
    1.25 +* HOL code generation: Scala as another target language.
    1.26  
    1.27 -* HOL: package for quotient types.
    1.28 +* HOL: partial_function definitions.
    1.29  
    1.30 -* HOL code generation: simple concept for abstract datatypes obeying
    1.31 -invariants (e.g. red-black trees).
    1.32 +* HOL: various tool enhancements, including Quickcheck, Nitpick,
    1.33 +  Sledgehammer, SMT integration.
    1.34  
    1.35 -* HOL: new development of the Reals using Cauchy Sequences.
    1.36 +* HOL: various additions to theory library, including HOL-Algebra,
    1.37 +  Imperative_HOL Multivariate_Analysis, Probability.
    1.38  
    1.39 -* HOL: reorganization of abstract algebra type class hierarchy.
    1.40 +* HOLCF: reorganization of library and related tools.
    1.41  
    1.42 -* HOL: substantial reorganization of main library and related tools.
    1.43 +* HOL/SPARK: interactive proof environment for verification conditions
    1.44 +  generated by the SPARK Ada program verifier.
    1.45  
    1.46 -* HOLCF: reorganization of 'domain' package.
    1.47 +* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
    1.48  
    1.49  
    1.50 -You may get Isabelle2009-2 from the following mirror sites:
    1.51 +You may get Isabelle2011 from the following mirror sites:
    1.52  
    1.53    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.54    Munich (Germany)     http://isabelle.in.tum.de/