ANNOUNCE
changeset 30848 c57b57546a07
parent 27085 dbf4f791953d
child 30890 0214d179c2be
     1.1 --- a/ANNOUNCE	Thu Apr 02 14:02:34 2009 +0200
     1.2 +++ b/ANNOUNCE	Thu Apr 02 14:02:45 2009 +0200
     1.3 @@ -1,35 +1,39 @@
     1.4 -Subject: Announcing Isabelle2008
     1.5 +Subject: Announcing Isabelle2009
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2008 is now available.
     1.9 +Isabelle2009 is now available.
    1.10  
    1.11 -This release consolidates Isabelle2007, see the NEWS file in the
    1.12 -distribution for more details.  Some notable improvements are:
    1.13 +This release significantly improves upon Isabelle2008, see the NEWS
    1.14 +file in the distribution for more details.  Some important changes
    1.15 +are:
    1.16  
    1.17 -* HOL: significant speedup of Metis prover; proper support for
    1.18 -multithreading.
    1.19 +* Complete re-implementation of locales, with proper support for local
    1.20 +syntax, and more robust interpretation mechanism.
    1.21  
    1.22 -* HOL: new version of 'primrec' command supporting type-inference and
    1.23 -local theory targets.
    1.24 +* New 'find_consts' and 'find_theorems' facilities, together with
    1.25 +"auto solve" feature of toplevel goal statements.
    1.26 +
    1.27 +* HOL: reorganization of main logic images.
    1.28  
    1.29 -* HOL: improved support for termination proofs of recursive function
    1.30 -definitions.
    1.31 +* HOL: improved implementation of Sledgehammer, based on generic ATP
    1.32 +manager; support for remote ATPs.
    1.33  
    1.34 -* New local theory targets for class instantiation and overloading.
    1.35 +* HOL: numerous library improvements.
    1.36  
    1.37 -* Support for named dynamic lists of theorems.
    1.38 +* Updated and extended versions of main reference manuals.
    1.39  
    1.40 -* Simple TTY interface with command-line editing.
    1.41 -
    1.42 -* Improved support for the Cygwin platform (Windows).
    1.43 +* Simplified arrangement of Isabelle startup scripts and settings
    1.44 +directory.
    1.45  
    1.46 -* Support for Poly/ML 5.2 with improved handling of multithreading and
    1.47 -external processes.
    1.48 +* Simplified internal programming interfaces for all Isar language
    1.49 +elements.
    1.50  
    1.51 -* Reorganized and updated version of Isabelle/Isar Reference Manual.
    1.52 +* General high-level support for concurrent ML programming.
    1.53 +
    1.54 +* Parallel proof checking within Isar theories.
    1.55  
    1.56  
    1.57 -You may get Isabelle2008 from the following mirror sites:
    1.58 +You may get Isabelle2009 from the following mirror sites:
    1.59  
    1.60    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.61    Munich (Germany)     http://isabelle.in.tum.de/