Subject: Announcing Isabelle2011
To: isabelle-users@cl.cam.ac.uk
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/