ANNOUNCE
changeset 11600 bbd6268e0b4b
parent 11109 ce1cefc6c14c
child 12927 b7c916bf3332
     1.1 --- a/ANNOUNCE	Thu Sep 27 18:46:32 2001 +0200
     1.2 +++ b/ANNOUNCE	Thu Sep 27 18:56:39 2001 +0200
     1.3 @@ -1,43 +1,18 @@
     1.4  
     1.5 -Subject: Announcing Isabelle99-2
     1.6 +Subject: Announcing Isabelle2001
     1.7  To: isabelle-users@cl.cam.ac.uk
     1.8  
     1.9 -Isabelle99-2 is now available.  This release continues the line of
    1.10 -Isabelle99, introducing various improvements in robustness and
    1.11 -usability.
    1.12 +Isabelle2001 is now available.
    1.13  
    1.14 -The most prominent highlights of Isabelle99-2 are as follows.  See the
    1.15 +The most prominent highlights of Isabelle2001 are as follows.  See the
    1.16  NEWS file distributed with Isabelle for more details.
    1.17  
    1.18 -  * Poly/ML 4.0 used by default
    1.19 -    More robust, less disk space required.
    1.20 -
    1.21 -  * Simplifier (Stefan Berghofer)
    1.22 -    Proper implementation as a derived rule, outside the kernel!
    1.23 -
    1.24 -  * Improved document preparation (Markus Wenzel)
    1.25 -    Near math-mode, sub/super scripts, more symbols etc.
    1.26 -
    1.27 -  * Isabelle/Isar (Markus Wenzel)
    1.28 -    Numerous usability improvements, e.g. support for initial
    1.29 -    schematic goals, failure prediction of subgoal statements,
    1.30 -    handling of non-atomic statements in induction.
    1.31 +  * Specific support for Poly/ML 4.1.1
    1.32 +    Faster, manages large heaps.
    1.33  
    1.34 -  * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
    1.35 -      Thomas M Rasmussen, Markus Wenzel)
    1.36 -    A collection of generic theories to be used together with main HOL.
    1.37 -
    1.38 -  * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
    1.39 -    General cleanup, more on nonstandard real analysis.
    1.40 +  * Meta-level proof terms (Stefan Berghofer)
    1.41  
    1.42 -  * HOL/Unix (Markus Wenzel)
    1.43 -    Some Aspects of Unix file-system security; demonstrates
    1.44 -    Isabelle/Isar in typical system modelling and verification tasks.
    1.45 -
    1.46 -  * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
    1.47 -    Extended version of the Isabelle/HOL tutorial.
    1.48 -
    1.49 -You may get Isabelle99-2 from any of the following mirror sites:
    1.50 +You may get Isabelle2001 from any of the following mirror sites:
    1.51  
    1.52    Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    1.53    Munich (Germany)  http://isabelle.in.tum.de/dist/