ANNOUNCE
author haftmann
Wed, 15 Jul 2009 10:11:13 +0200
changeset 32073 0a83608e21f1
parent 30897 44cba7df4003
child 33842 efa1b89c79e0
permissions -rw-r--r--
additional preprocessor rule

Subject: Announcing Isabelle2009
To: isabelle-users@cl.cam.ac.uk

Isabelle2009 is now available.

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

* Complete re-implementation of locales, with proper support for local
syntax, and more general locale expressions.

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

* Simplified programming interfaces for all Isar language elements.

* 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)       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/