changeset 37159 07f3f5a03e98
parent 33914 d17f447fec02
child 37317 5164c4ec787b
--- a/ANNOUNCE	Thu May 27 21:37:42 2010 +0200
+++ b/ANNOUNCE	Fri May 28 11:23:34 2010 +0200
@@ -1,48 +1,16 @@
-Subject: Announcing Isabelle2009-1
+Subject: Announcing Isabelle2009-2
-Isabelle2009-1 is now available.
+Isabelle2009-2 is now available.
-This release improves upon Isabelle2009 in many ways, see the NEWS
-file in the distribution for more details.  Some important changes
+This release improves upon Isabelle2009-1 in many respects, see the
+NEWS file in the distribution for more details.  Some notable changes
-* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
-on a given logic image.
-* HOL-SMT: proof method "smt" for a combination of first-order logic
-with equality, linear and nonlinear (natural/integer/real) arithmetic,
-and fixed-size bitvectors.
-* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
-* HOL: counterexample generator tool Nitpick based on the Kodkod
-relational model finder.
-* HOL: predicate compiler turning inductive into (executable)
-equational specifications.
-* HOL: refined number theory.
-* HOL: various parts of multivariate analysis.
-* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
-arithmetic, based on external semidefinite programming solvers.
-* HOLCF: new definitional domain package.
-* Revised tutorial on locales.
-* ML: tacticals for subgoal focus.
-* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
-errors and run-time exceptions, including detailed source positions.
-* Parallel checking of nested Isar proofs, with improved scalability
-up to 8 cores.
-You may get Isabelle2009-1 from the following mirror sites:
+You may get Isabelle2009-2 from the following mirror sites:
   Cambridge (UK)
   Munich (Germany)