|NOTICE, please do not remove from top of page.|
|I released this article to Citizendium. In particular, the identical text that appears there is of my sole authorship. Therefore, no credit for Citizendium content on the Knowino applies.|
|Boris Tsirelson 15:16, 18 December 2010 (EST)|
Now available: Isabelle2011
- 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).