author haftmann
Mon, 23 Nov 2009 19:03:16 +0100
changeset 33866 34e45b2afe43
parent 33842 efa1b89c79e0
child 33873 e9120a7b2779
permissions -rw-r--r--

Subject: Announcing Isabelle2009-1

Isabelle2009-1 is now available.

This release improves upon Isabelle2009 in many ways, see the NEWS
file in the distribution for more details.  Some important changes

* Proof method "smt" for a combination of first-order logic with equality,
linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors.

* Counterexample generator tool »nitpick« based on the Kodkod relational model finder.

* Predicate compiler turning inductive into (executable) equational specifications.

* Refined number theory.

* Various parts of multivariate analysis.

* HOL-Boogie: an interactive prover back-end for Boogie and VCC.

* Revised tutorial on locales.

* New definitional domain package for HOLCF.

* Support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.

You may get Isabelle2009-1 from the following mirror sites:

  Cambridge (UK)
  Munich (Germany)
  Sydney (Australia)