Email Gateway (Aug 22 2022 at 09:56): Email Gateway (Aug 22 2022 at 09:56):From: Makarius <makarius@sketis.net>
Isabelle2015 is now available.
This version improves upon Isabelle2014 in many ways, see the NEWS file in
the distribution for more details. Some important points are as follows.
Improved Isabelle/jEdit Prover IDE: folding / bracket matching for Isar,
support for BibTeX files, improved graphview panel, improved scheduling for
asynchronous print commands (e.g. Sledgehammer provers).
Support for 'private' and 'qualified' name space modifiers.
Structural composition of proof methods (meth1; meth2) in Isar.
HOL: BNF datatypes and codatatypes are now standard.
HOL: numerous tool improvements: Nitpick, Sledgehammer, SMT, including a
new free (!) version of Z3.
HOL: numerous library refinements and enhancements.
New proof method "rewrite" for single-step rewriting with subterm
selection based on patterns.
New Eisbach proof method language and "match" method.
Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer,
system.
You may get Isabelle2015 from the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/
Email Gateway (Aug 22 2022 at 09:56):From: Larry Paulson <lp15@cam.ac.uk>
Many thanks, as always, to Makarius for organising this release!
I’d like to take this opportunity to plug my own contributions:
Complex powers and square roots.
New library of properties of the complex transcendental functions sin,
cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.
Larry
Last updated: Nov 21 2024 at 12:39 UTC