author wenzelm
Tue, 02 Oct 2018 19:02:47 +0200
changeset 69103 814a1ab42d70
parent 68648 371e814af6f0
child 70032 0674c24afc5e
permissions -rw-r--r--
unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;

Subject: Announcing Isabelle2018

Isabelle2018 is now available.

This version introduces many changes over Isabelle2017: see the NEWS
file for further details. Here are some notable points:

* Improved infix notation within terms.

* Improved syntax for formal comments, within terms and other languages.

* Improved management of ROOT files and session-qualified theories.

* Various improvements of document preparation.

* Many Isabelle/jEdit improvements, including semantic IDE for BibTeX.

* Numerous HOL library improvements, including HOL-Algebra.

* Substantial additions to HOL-Analysis.

* HOL-Library.Code_Lazy: code generation for lazy evaluation.

* HOL-Real_Asymp: tools for semi-automatic real asymptotics.

* Isabelle server for reactive communication with other programs.

* More uniform 64-bit platform support: smaller Isabelle application.

You may get Isabelle2018 from the following mirror sites:

  Cambridge (UK)
  Munich (Germany)
  Sydney (Australia)
  Potsdam, NY (USA)