ANNOUNCE
changeset 33842 efa1b89c79e0
parent 30897 44cba7df4003
child 33866 34e45b2afe43
equal deleted inserted replaced
33841:6508d0e8bb19 33842:efa1b89c79e0
     1 Subject: Announcing Isabelle2009
     1 Subject: Announcing Isabelle2009-1
     2 To: isabelle-users@cl.cam.ac.uk
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     3 
     4 Isabelle2009 is now available.
     4 Isabelle2009-1 is now available.
     5 
     5 
     6 This release significantly improves upon Isabelle2008, see the NEWS
     6 This release improves upon Isabelle2009 in many ways, see the NEWS
     7 file in the distribution for more details.  Some important changes
     7 file in the distribution for more details.  Some important changes
     8 are:
     8 are:
     9 
     9 
    10 * Complete re-implementation of locales, with proper support for local
    10 * FIXME
    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 
    11 
    36 
    12 
    37 You may get Isabelle2009 from the following mirror sites:
    13 You may get Isabelle2009-1 from the following mirror sites:
    38 
    14 
    39   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    15   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    40   Munich (Germany)     http://isabelle.in.tum.de/
    16   Munich (Germany)     http://isabelle.in.tum.de/
    41   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/
    17   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/