ANNOUNCE
author desharna
Wed, 25 May 2022 15:49:12 +0200
changeset 75960 15483f001222
parent 75320 c2a2be496f35
permissions -rw-r--r--
redefined order.{,strict_}mono as abbreviations of monotone

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

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)       https://www.cl.cam.ac.uk/research/hvg/Isabelle
  Munich (Germany)     https://isabelle.in.tum.de
  Sydney (Australia)   https://mirror.cse.unsw.edu.au/pub/isabelle
  Potsdam, NY (USA)    https://mirror.clarkson.edu/isabelle