ANNOUNCE
author hoelzl
Mon, 08 Aug 2016 14:13:14 +0200
changeset 63627 6ddb43c6b711
parent 62197 f354900ac0ea
child 64072 9f96e4da3064
permissions -rw-r--r--
rename HOL-Multivariate_Analysis to HOL-Analysis.

Subject: Announcing Isabelle2016
To: isabelle-users@cl.cam.ac.uk

Isabelle2016 is now available.

This version improves upon Isabelle2015 in many ways, see the NEWS file in the
distribution for further details. Some highlights are as follows:

* Enhanced Isabelle/jEdit Prover IDE, with separate State versus Output panel
and more asynchronous task management within the prover/GUI.

* Additional Isar language elements for structured statements and proofs.

* Document language refinements, with Markdown-like text structure.

* More Isabelle symbols in theory and document sources.

* Pure/HOL: uniform treatment of overloaded constant definitions versus type
definitions; upgrade of HOL typedef to definitional principle.

* HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.

* HOL library additions and improvements, notably HOL-Multivariate_Analysis,
HOL-Probability, HOL-Data_Structures.

* Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard
ML), per-thread profiling, native Windows version (32bit and 64bit).


You may get Isabelle2016 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
  Potsdam, NY (USA)    http://mirror.clarkson.edu/isabelle