Email Gateway (Dec 13 2021 at 14:40): Email Gateway (Dec 13 2021 at 14:40):From: Makarius <makarius@sketis.net>
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
Email Gateway (Dec 13 2021 at 20:35):From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Dear Mac Isabelle users,
I have just updated my IsabelleJedit Mac application with a new version that opens Isabelle 2021-1.
https://github.com/Frederic-Boulanger-UPS/MacIsabelle2021-1App <https://github.com/Frederic-Boulanger-UPS/MacIsabelle2021-1App>
Please look at the README file to see how to handle "damaged application" or other security related messages that prevent you from launching the application on MacOS (you may have to use the Terminal).
Do not hesitate to look at the script inside the application (with "Show package contents", then inspect Contents/Resources/Scripts/main.scpt) to check what the application does before authorising its execution on your Mac (you are not required to trust me).
Hoping this may be useful,
Frédéric
Frédéric Boulanger
CentraleSupélec - Département Informatique Laboratoire Méthodes Formelles (LMF)
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex Bât. 650 - 1 rue Raimond Castaing, 91190 Gif-sur-Yvette
+33 [0]1 69 85 14 84
Last updated: Jan 04 2025 at 20:18 UTC