Email Gateway (Aug 18 2022 at 11:02): Email Gateway (Aug 18 2022 at 11:02):From: Makarius <makarius@sketis.net>
Isabelle2007 is finally available.
This release introduces fundamental changes over Isabelle2005, see the
NEWS file in the distribution for more details. Numerous existing
concepts have been generalized and re-implemented based on novel
system architecture. New theories and proof tools have been added
(mostly for HOL). Some highlights are:
Support for nominal datatypes (binding structures) due to the
HOL-Nominal logic.
General local theory infrastructure for specifications depending on
parameters and assumptions (e.g. from locales, classes).
New basic specification elements 'definition', 'axiomatization',
'abbreviation', 'notation'.
New version of 'inductive' package for inductive predicates;
separate variant 'inductive_set'.
New 'function' package for general recursive function definitions.
New 'class' package combination of axclass + locale interpretation.
Built-in Metis prover, external linkup for automated provers, and
'sledgehammer' command for automated proof synthesis.
Auto quickcheck: toplevel goals are tested for counterexamples
automatically when they are stated.
Second generation code generator for a subset of HOL, targeting SML,
Haskell, and OCaml.
Command 'normal_form' and method "normalization" for evaluating
terms with free variables.
Full list comprehension syntax for HOL.
Much improved algebraic capabilities, including Groebner bases.
Embedding of ML code into theories with static references to the
logical context (via antiquotations).
Parallel loading of theories based on native multicore support in
Poly/ML 5.1.
You may get Isabelle2007 from the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
Email Gateway (Aug 18 2022 at 11:02):From: Makarius <makarius@sketis.net>
Our third mirror is now also up-to-date:
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/
Makarius
Last updated: Nov 21 2024 at 12:39 UTC