author wenzelm
Tue, 14 Apr 2009 15:41:40 +0200
changeset 30890 0214d179c2be
parent 30848 c57b57546a07
child 30894 49c14e3cdc4b
permissions -rw-r--r--
added Haskabelle -- in accordance to website/index.html version f397b96e3ad2;

Subject: Announcing Isabelle2009

Isabelle2009 is now available.

This release significantly improves upon Isabelle2008, see the NEWS
file in the distribution for more details.  Some important changes

* Complete re-implementation of locales, with proper support for local
syntax, and more robust interpretation mechanism.

* New 'find_consts' and 'find_theorems' facilities, together with
"auto solve" feature of toplevel goal statements.

* HOL: reorganization of main logic images.

* HOL: improved implementation of Sledgehammer, based on generic ATP
manager; support for remote ATPs.

* HOL: numerous library improvements.

* Updated and extended versions of main reference manuals.

* Simplified arrangement of Isabelle startup scripts and settings

* Simplified internal programming interfaces for all Isar language

* General high-level support for concurrent ML programming.

* Parallel proof checking within Isar theories.

* Haskabelle importer from Haskell source files to Isar theories.

You may get Isabelle2009 from the following mirror sites:

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