ANNOUNCE

improved abs_def: only abstract over outermost (unique) Vars;

+
−Subject: Announcing Isabelle2007
+
−To: [e-mail]
+
−
+
−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).
+
−
+
−The main highlights are:
+
−
+
−* Fully featured 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.
+
−
+
−* Various improvements in locale infrastructure (interpretation etc.)
+
−
+
−* Various improvements of Isar language elements and related proof
+
−tools.
+
−
+
−* Built-in Metis prover, external linkup for automated provers, and
+
−'sledghammer' command for automated proof synthesis.
+
−
+
−* Second generation code-generator for a subset of HOL, targeting SML,
+
−Haskell, and OCaml.
+
−
+
−* Improved support for arbitrary ML operations depending on the
+
−logical context.
+
−
+
−* 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/
+
−  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/