author wenzelm
Mon, 01 Oct 2007 21:19:49 +0200
changeset 24802 6bd8ec8f3fc8
parent 17696 eccdee8a0790
child 24813 74bc59c2c4a6
permissions -rw-r--r--
preliminary material for Isabelle2007;

Subject: Announcing Isabelle2007

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:

* New 'function' package for general recursive function definitions.

* New version of 'inductive' package for inductive predicates;
separate variant 'inductive_set'.

* New basic specification elements 'definition', 'axiomatization',
'abbreviation', 'notation'.

* New 'class' package combination of axclass + locale interpretation.

* Fully featured support for nominal datatypes (binding structures)
due to the HOL-Nominal logic.

* Various improvements in locale infrastructure (interpretation etc.)

* Various improvements of Isar language elements and related proof

* Built-in Metis prover, external linkup for automated provers, and
'sledghammer' command for automated proof synthesis.

* General local theory infrastructure for specifications depending on
parameters and assumptions (e.g. from locales, classes).

* 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)
  Munich (Germany)
  Sydney (Australia)