ANNOUNCE
changeset 27066 dbf97292e5fd
parent 27061 a057cb0d7d55
child 27085 dbf4f791953d
     1.1 --- a/ANNOUNCE	Tue Jun 03 13:17:11 2008 +0200
     1.2 +++ b/ANNOUNCE	Tue Jun 03 14:04:26 2008 +0200
     1.3 @@ -6,16 +6,19 @@
     1.4  This release consolidates Isabelle2007, see the NEWS file in the
     1.5  distribution for more details.  Some notable improvements are:
     1.6  
     1.7 -* New version of HOL 'primrec' supporting type-inference and local
     1.8 -theory targets.
     1.9 +* HOL: significant speedup of Metis prover; proper support for
    1.10 +multithreading.
    1.11 +
    1.12 +* HOL: new version of 'primrec' command supporting type-inference and
    1.13 +local theory targets.
    1.14 +
    1.15 +* HOL: improved support for termination proofs of recursive function
    1.16 +definitions.
    1.17  
    1.18  * New local theory targets for class instantiation and overloading.
    1.19  
    1.20  * Support for named dynamic lists of theorems.
    1.21  
    1.22 -* Significant speedup of Metis prover, with proper support for
    1.23 -multithreading.
    1.24 -
    1.25  * Simple TTY interface with command-line editing.
    1.26  
    1.27  * Improved support for the Cygwin platform (Windows).
    1.28 @@ -23,7 +26,7 @@
    1.29  * Support for Poly/ML 5.2 with improved handling of multithreading and
    1.30  external processes.
    1.31  
    1.32 -* Reorganized version of Isabelle/Isar Reference Manual.
    1.33 +* Reorganized and updated version of Isabelle/Isar Reference Manual.
    1.34  
    1.35  
    1.36  You may get Isabelle2008 from the following mirror sites: