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