[isabelle] 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)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
  Munich (Germany)     http://isabelle.in.tum.de/
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.