author wenzelm
Sat, 02 Aug 2014 19:29:02 +0200
changeset 57843 d8966c09025c
parent 57524 b8448367f9c7
child 60016 6e6cc8c012a2
permissions -rw-r--r--
proper priority for error over warning also for node_status (see 9c5220e05e04);

Subject: Announcing Isabelle2014

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

* 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)
  Munich (Germany)
  Sydney (Australia)