author blanchet
Mon, 31 Jan 2022 16:09:23 +0100
changeset 75020 b087610592b4
parent 74913 c2a2be496f35
child 76108 bdab17df07a9
permissions -rw-r--r--
rationalized output for forthcoming slicing model

Subject: Announcing Isabelle2021-1

Isabelle2021-1 is now available.

This version introduces many changes over Isabelle2020-1: see the NEWS
file for further details. Here are various details:

* HTML presentation now includes links to formal entities.

* Isar: local theory support for 'syntax' and 'no_syntax' commands.

* Isabelle/jEdit: distribution of original jEdit editor with Isabelle/Scala
modules and plugins.

* HOL: new order prover.

* HOL: many changes and improvements on bit operations and word types.

* HOL: various library improvements (HOL-Library, HOL-Combinatorics,
HOL-Analysis, HOL-Statespace)

* Sledgehammer: update of ATPs and SMTs: E prover, veriT, Zipperposition,
Vampire (now with Open-Source license).

* Nitpick: external MiniSat solver for all supported Isabelle platforms.

* ML: uniform treatment of external processes via Isabelle/Scala.

* ML: advanced antiquotations for Type/Const constructors, and for inline
instantiation of types, terms, facts.

* Haskell: substantially improved Isabelle/Haskell library.

* System: more predefined Isabelle symbols (blackboard-bold, Z notation).

* System: support for Isabelle/Scala modules defined in user-space.

* System: improved document preparation using Isabelle/Scala.

* System: update to current Java 17 LTS.

* System: update to Poly/ML 5.9 with improved support for ARM64 on Linux.

You may get Isabelle2021-1 from the following mirror sites:

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