ANNOUNCE
author blanchet
Sun, 26 May 2013 14:02:03 +0200
changeset 52151 de43876e77bf
parent 51051 4f89c21ca567
child 53978 65c893e0849f
permissions -rw-r--r--
disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)

Subject: Announcing Isabelle2013
To: isabelle-users@cl.cam.ac.uk

Isabelle2013 is now available.

This version consolidates Isabelle2012 and introduces numerous
improvements, see the NEWS file in the distribution for more details.
Some highlights are:

* Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.

* Advanced build tool based on Isabelle/Scala.

* Updated manuals: isar-ref, implementation, system.

* Pure: improved support for block-structured specification contexts.

* HOL tool enhancements: Sledgehammer, Lifting, Quickcheck.

* HOL library enhancements: HOL-Library, HOL-Probability, HOL-Cardinals.

* HOL: New BNF-based (co)datatype package.

* Improved performance thanks to Poly/ML 5.5.0.


You may get Isabelle2013 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/