updated for release;
Mon, 01 Nov 2021 15:49:03 +0100
changeset 74651 81cc8f2ea9e7
parent 74650 e911be103066
child 74652 72d2ef5ee128
updated for release;
--- a/ANNOUNCE	Mon Nov 01 15:24:53 2021 +0100
+++ b/ANNOUNCE	Mon Nov 01 15:49:03 2021 +0100
@@ -1,37 +1,46 @@
-Subject: Announcing Isabelle2021
+Subject: Announcing Isabelle2021-1
 To: isabelle-users@cl.cam.ac.uk
-Isabelle2021 is now available.
+Isabelle2021-1 is now available.
-This version introduces many changes over Isabelle2020: see the NEWS
+This version introduces many changes over Isabelle2020-1: see the NEWS
 file for further details. Here are various details:
-* Improved HTML presentation in Isabelle/Scala, using PIDE markup.
+* Isar: local theory support for 'syntax' and 'no_syntax' commands.
-* Improved PDF document preparation in Isabelle/Scala, using LuaLaTeX.
+* Isabelle/jEdit: distribution of original jEdit editor with Isabelle/Scala
+modules and plugins.
-* Isabelle/jEdit: improved monitoring of Java and ML process.
+* HOL: new order prover.
-* Isabelle/jEdit: improved look-and-feel and IDE feedback.
+* HOL: many changes and improvements on bit operations and word types.
-* Pure: improved handling of named contexts and local syntax bundles.
+* HOL: various library improvements (HOL-Library, HOL-Combinatorics,
+HOL-Analysis, HOL-Statespace)
-* HOL: substantially reworked support for Word library.
+* Sledgehammer: update of ATPs and SMTs: E prover, veriT, Zipperposition,
+Vampire (now with Open-Source license).
-* HOL: various syntax and library improvements.
+* Nitpick: external MiniSat solver for all supported Isabelle platforms.
+* ML: uniform treatment of external processes via Isabelle/Scala.
-* HOL: various Sledgehammer and SMT improvements, with updated external tools.
+* ML: advanced antiquotations for Type/Const constructors, and for inline
+instantiation of types, terms, facts.
-* HOL: support for Nitpick/Kodkod in Isabelle/Scala.
+* Haskell: substantially improved Isabelle/Haskell library.
-* ML: routine support for Isabelle/Scala functions in Isabelle/ML.
+* System: more predefined Isabelle symbols (blackboard-bold, Z notation).
+* System: support for Isabelle/Scala modules defined in user-space.
-* System: support for Isabelle/Scala services defined in user-space.
+* System: improved document preparation using Isabelle/Scala.
-* Support for macOS Big Sur on Intel and Apple Silicon (ARM).
+* System: update to current OpenJDK 17 (LTS) and Poly/ML 5.9 (with preliminary
+support for arm64).
-You may get Isabelle2021 from the following mirror sites:
+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
--- a/NEWS	Mon Nov 01 15:24:53 2021 +0100
+++ b/NEWS	Mon Nov 01 15:49:03 2021 +0100
@@ -153,6 +153,8 @@
 *** HOL ***
+* New order prover.
 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to
 "order.antisym" and "order.eq_iff", to coexist locally with "antisym"
 and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant