diff -r 4dedb6e2dac2 -r bdab17df07a9 ANNOUNCE --- a/ANNOUNCE Sat Sep 10 16:12:52 2022 +0200 +++ b/ANNOUNCE Sat Sep 10 16:57:12 2022 +0200 @@ -1,49 +1,35 @@ -Subject: Announcing Isabelle2021-1 +Subject: Announcing Isabelle2022 To: isabelle-users@cl.cam.ac.uk -Isabelle2021-1 is now available. +Isabelle2022 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. +This version introduces notable changes over Isabelle2021-1: see the +NEWS file for further details. Here are various details: -* Isabelle/jEdit: distribution of original jEdit editor with Isabelle/Scala -modules and plugins. +* HTML presentation is more robust and covers more files and links. -* HOL: new order prover. +* Display of instantiation for schematic goals. -* HOL: many changes and improvements on bit operations and word types. +* PIDE: improved Isabelle/VSCode based on bundled VSCodium engine. -* HOL: various library improvements (HOL-Library, HOL-Combinatorics, -HOL-Analysis, HOL-Statespace) +* HOL: various improvements of theory libraries. -* 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. +* HOL: updates and improvements of Sledgehammer. -* ML: uniform treatment of external processes via Isabelle/Scala. +* HOL: improved simproc support for record types. -* ML: advanced antiquotations for Type/Const constructors, and for inline -instantiation of types, terms, facts. +* ML: scalable type Bytes.T with support for XZ compression. -* Haskell: substantially improved Isabelle/Haskell library. +* System: bundled Node.js/Chromium/Electron platform (part VSCodium). -* System: more predefined Isabelle symbols (blackboard-bold, Z notation). - -* System: support for Isabelle/Scala modules defined in user-space. +* System: Isabelle/Scala is based on Scala 3 (dotty compiler). -* System: improved document preparation using Isabelle/Scala. +* System: tools to sync hg repositories, notably Isabelle + AFP. -* System: update to current Java 17 LTS. - -* System: update to Poly/ML 5.9 with improved support for ARM64 on Linux. +* System: improved "isabelle log" tool with regex filtering. -You may get Isabelle2021-1 from the following mirror sites: +You may get Isabelle2022 from the following mirror sites: Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle Munich (Germany) https://isabelle.in.tum.de