ANNOUNCE
author wenzelm
Fri, 08 Jul 2011 22:00:53 +0200
changeset 43713 1ba5331b4623
parent 41605 7d035da21e9c
child 44801 a0459c50cfc9
permissions -rw-r--r--
moved global state to structure Document (again);

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/