author wenzelm
Mon, 17 Jan 2011 22:57:17 +0100
changeset 41605 7d035da21e9c
parent 41604 313b0033034a
child 44801 a0459c50cfc9
permissions -rw-r--r--

Subject: Announcing Isabelle2011

Isabelle2011 is now available.

This version significantly improves upon Isabelle2009-2, see the NEWS
file in the distribution for more details.  Some notable changes are:

* Experimental Prover IDE based on Isabelle/Scala and jEdit.

* Coercive subtyping (configured in HOL/Complex_Main).

* HOL code generation: Scala as another target language.

* HOL: partial_function definitions.

* HOL: various tool enhancements, including Quickcheck, Nitpick,
  Sledgehammer, SMT integration.

* HOL: various additions to theory library, including HOL-Algebra,
  Imperative_HOL, Multivariate_Analysis, Probability.

* HOLCF: reorganization of library and related tools.

* HOL/SPARK: interactive proof environment for verification conditions
  generated by the SPARK Ada program verifier.

* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).

You may get Isabelle2011 from the following mirror sites:

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