ANNOUNCE
author wenzelm
Wed Apr 15 19:52:45 2009 +0200 (2009-04-15)
changeset 30897 44cba7df4003
parent 30894 49c14e3cdc4b
child 33842 efa1b89c79e0
permissions -rw-r--r--
tuned;
     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 general locale expressions.
    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 programming interfaces for all Isar language elements.
    29 
    30 * General high-level support for concurrent ML programming.
    31 
    32 * Parallel proof checking within Isar theories.
    33 
    34 * Haskabelle importer from Haskell source files to Isar theories.
    35 
    36 
    37 You may get Isabelle2009 from the following mirror sites:
    38 
    39   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    40   Munich (Germany)     http://isabelle.in.tum.de/
    41   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/