author haftmann
Mon, 29 Oct 2007 16:46:22 +0100
changeset 25228 59afe8a0a7e1
parent 25213 48a1e80f5cdb
child 25229 2673709fb8f7
permissions -rw-r--r--
added nbe

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:

* 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
'sledghammer' command for automated proof synthesis.

* Full list comprehension syntax.

* Various improvements in locale infrastructure (interpretation etc.)

* Various improvements of Isar language elements and related proof

* 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.

* 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.

* Improved algebraic capabilities by means of semiring normalization,
Groebner bases and Ferrante/Rackoff algorithm.

You may get Isabelle2007 from the following mirror sites:

  Cambridge (UK)
  Munich (Germany)
  Sydney (Australia)