From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle2014 is now available.
This version significantly improves upon Isabelle2013-2, see the NEWS
file in the distribution for more details. Some highlights are:
Improved Isabelle/jEdit Prover IDE: navigation, completion,
spell-checking, Query panel, Simplifier Trace panel.
Support for auxiliary files within the Prover IDE, notably
Isabelle/ML.
Support for official Standard ML within the Prover IDE,
independently of Isabelle theory and proof development.
HOL: BNF datatypes and codatatypes within theory Main, with numerous
add-on tools.
HOL tool enhancements: Nitpick, Sledgehammer.
HOL: internal SAT solver "cdclite" with models and proof traces.
HOL: updated SMT module, with support for SMT-LIB 2 and recent
versions of Z3, as well as CVC3, CVC4.
HOL: numerous library enhancements: main HOL, HOL-Word,
HOL-Multivariate_Analysis, HOL-Probability.
System integration: improved support of LaTeX on Windows platform.
Updated and extended manuals: codegen, datatypes, implementation,
isar-ref, jedit, system.
You may get Isabelle2014 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