diff r 04c560b4ebc1 r e9120a7b2779 ANNOUNCE
 a/ANNOUNCE Mon Nov 23 22:35:54 2009 +0100
+++ b/ANNOUNCE Mon Nov 23 22:47:08 2009 +0100
@@ 7,24 +7,35 @@
file in the distribution for more details. Some important changes
are:
* Proof method "smt" for a combination of firstorder logic with equality,
linear and nonlinear (natural/integer/real) arithmetic, and fixedsize bitvectors.

* Counterexample generator tool »nitpick« based on the Kodkod relational model finder.
+* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
+on a given logic image.
* Predicate compiler turning inductive into (executable) equational specifications.

* Refined number theory.

* Various parts of multivariate analysis.
+* HOLSMT: proof method "smt" for a combination of firstorder logic
+with equality, linear and nonlinear (natural/integer/real) arithmetic,
+and fixedsize bitvectors.
* HOLBoogie: an interactive prover backend 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.
+
+* HOLCF: new definitional domain package.
+
* Revised tutorial on locales.
* New definitional domain package for HOLCF.
+* Support for Poly/ML 5.3.0, with improved reporting of compiler
+errors and runtime exceptions, including detailed source positions.
* Support for Poly/ML 5.3.0, with improved reporting of compiler errors and runtime exceptions, including detailed source positions.
+* Parallel checking of nested Isar proofs, with improved scalability
+up to 8 cores.
+
You may get Isabelle20091 from the following mirror sites: