ANNOUNCE

more robust build on midrange hardware;

+
−Subject: Announcing Isabelle2021-1
+
−To: [e-mail]
+
−
+
−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 OpenJDK 17 (LTS) and Poly/ML 5.9 (with preliminary
+
−support for arm64).
+
−
+
−
+
−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