Email Gateway (Aug 18 2022 at 16:52): Email Gateway (Aug 18 2022 at 16:52):From: Makarius <makarius@sketis.net>
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/
Last updated: Nov 21 2024 at 12:39 UTC