ANNOUNCE
 changeset 33873 e9120a7b2779 parent 33866 34e45b2afe43 child 33881 d8958955ecb5
```     1.1 --- a/ANNOUNCE	Mon Nov 23 22:35:54 2009 +0100
1.2 +++ b/ANNOUNCE	Mon Nov 23 22:47:08 2009 +0100
1.3 @@ -7,24 +7,35 @@
1.4  file in the distribution for more details.  Some important changes
1.5  are:
1.6
1.7 -* Proof method "smt" for a combination of first-order logic with equality,
1.8 -linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors.
1.9 -
1.10 -* Counterexample generator tool »nitpick« based on the Kodkod relational model finder.
1.11 +* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
1.12 +on a given logic image.
1.13
1.14 -* Predicate compiler turning inductive into (executable) equational specifications.
1.15 -
1.16 -* Refined number theory.
1.17 -
1.18 -* Various parts of multivariate analysis.
1.19 +* HOL-SMT: proof method "smt" for a combination of first-order logic
1.20 +with equality, linear and nonlinear (natural/integer/real) arithmetic,
1.21 +and fixed-size bitvectors.
1.22
1.23  * HOL-Boogie: an interactive prover back-end for Boogie and VCC.
1.24
1.25 +* HOL: Counterexample generator tool Nitpick based on the Kodkod
1.26 +relational model finder.
1.27 +
1.28 +* HOL: predicate compiler turning inductive into (executable)
1.29 +equational specifications.
1.30 +
1.31 +* HOL: refined number theory.
1.32 +
1.33 +* HOL: various parts of multivariate analysis.
1.34 +
1.35 +* HOLCF: new definitional domain package.
1.36 +
1.37  * Revised tutorial on locales.
1.38
1.39 -* New definitional domain package for HOLCF.
1.40 +* Support for Poly/ML 5.3.0, with improved reporting of compiler
1.41 +errors and run-time exceptions, including detailed source positions.
1.42
1.43 -* Support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.
1.44 +* Parallel checking of nested Isar proofs, with improved scalability
1.45 +up to 8 cores.
1.46 +
1.47
1.48  You may get Isabelle2009-1 from the following mirror sites:
1.49
```