ANNOUNCE
author wenzelm
Tue Apr 14 15:41:40 2009 +0200 (2009-04-14)
changeset 30890 0214d179c2be
parent 30848 c57b57546a07
child 30894 49c14e3cdc4b
permissions -rw-r--r--
added Haskabelle -- in accordance to website/index.html version f397b96e3ad2;
     1 Subject: Announcing Isabelle2009
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     4 Isabelle2009 is now available.
     5 
     6 This release significantly improves upon Isabelle2008, see the NEWS
     7 file in the distribution for more details.  Some important changes
     8 are:
     9 
    10 * Complete re-implementation of locales, with proper support for local
    11 syntax, and more robust interpretation mechanism.
    12 
    13 * New 'find_consts' and 'find_theorems' facilities, together with
    14 "auto solve" feature of toplevel goal statements.
    15 
    16 * HOL: reorganization of main logic images.
    17 
    18 * HOL: improved implementation of Sledgehammer, based on generic ATP
    19 manager; support for remote ATPs.
    20 
    21 * HOL: numerous library improvements.
    22 
    23 * Updated and extended versions of main reference manuals.
    24 
    25 * Simplified arrangement of Isabelle startup scripts and settings
    26 directory.
    27 
    28 * Simplified internal programming interfaces for all Isar language
    29 elements.
    30 
    31 * General high-level support for concurrent ML programming.
    32 
    33 * Parallel proof checking within Isar theories.
    34 
    35 * Haskabelle importer from Haskell source files to Isar theories.
    36 
    37 
    38 You may get Isabelle2009 from the following mirror sites:
    39 
    40   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    41   Munich (Germany)     http://isabelle.in.tum.de/
    42   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/