1 Subject: Announcing Isabelle2014
2 To: isabelle-users@cl.cam.ac.uk
4 Isabelle2014 is now available.
6 This version significantly improves upon Isabelle2013-2, see the NEWS
7 file in the distribution for more details. Some highlights are:
9 * Improved Isabelle/jEdit Prover IDE: navigation, completion,
10 spell-checking, Query panel, Simplifier Trace panel.
12 * Support for auxiliary files within the Prover IDE.
14 * Support for official Standard ML within the Prover IDE,
15 independently of Isabelle theory and proof development.
17 * HOL: BNF datatypes and codatatypes within theory Main, with numerous
20 * HOL tool enhancements: Nitpick, Sledgehammer.
22 * HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis,
25 * HOL: internal SAT solver "cdclite" with models and proof traces.
27 * HOL: updated SMT module, with support for SMT-LIB 2 and recent
28 versions of Z3, as well as CVC3, CVC4.
30 * Updated and extended manuals: codegen, datatypes, implementation,
31 isar-ref, jedit, system.
33 * System integration: improved support of LateX on Windows platform.
36 You may get Isabelle2013-2 from the following mirror sites:
38 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
39 Munich (Germany) http://isabelle.in.tum.de/
40 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/