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: improved support for termination proofs of recursive function
    1.28 -definitions.
    1.29 +* HOL: reorganization of main logic images.
    1.30  
    1.31 -* New local theory targets for class instantiation and overloading.
    1.32 +* HOL: improved implementation of Sledgehammer, based on generic ATP
    1.33 +manager; support for remote ATPs.
    1.34  
    1.35 -* Support for named dynamic lists of theorems.
    1.36 +* HOL: numerous library improvements.
    1.37  
    1.38 -* Simple TTY interface with command-line editing.
    1.39 +* Updated and extended versions of main reference manuals.
    1.40  
    1.41 -* Improved support for the Cygwin platform (Windows).
    1.42 +* Simplified arrangement of Isabelle startup scripts and settings
    1.43 +directory.
    1.44  
    1.45 -* Support for Poly/ML 5.2 with improved handling of multithreading and
    1.46 -external processes.
    1.47 +* Simplified internal programming interfaces for all Isar language
    1.48 +elements.
    1.49  
    1.50 -* Reorganized and updated version of Isabelle/Isar Reference Manual.
    1.51 +* General high-level support for concurrent ML programming.
    1.52  
    1.53 +* Parallel proof checking within Isar theories.
    1.54  
    1.55 -You may get Isabelle2008 from the following mirror sites:
    1.56 +
    1.57 +You may get Isabelle2009 from the following mirror sites:
    1.58  
    1.59    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.60    Munich (Germany)     http://isabelle.in.tum.de/