ANNOUNCE
changeset 12964 2ac9265b2cd5
parent 12927 b7c916bf3332
child 12983 7d13480ee668
     1.1 --- a/ANNOUNCE	Wed Feb 27 15:23:42 2002 +0100
     1.2 +++ b/ANNOUNCE	Wed Feb 27 18:41:28 2002 +0100
     1.3 @@ -4,20 +4,27 @@
     1.4  
     1.5  Isabelle2002 is now available.
     1.6  
     1.7 -This release clarifies long-standing issues at large, providing of
     1.8 -more comfortable and robust environment.
     1.9 +In this release many important aspects of Isabelle have been reworked
    1.10 +to improve robustness and usability (this occasionally causes
    1.11 +incompatibility with earlier versions).
    1.12  
    1.13 -In this release a lot of important issues of existing concepts 
    1.14 +The most prominent highlights of Isabelle2002 are as follows; see the
    1.15 +NEWS of the distribution for more details.
    1.16 +
    1.17 +  * The Isabelle/HOL tutorial has been published as LNCS 2283;
    1.18 +    Isabelle2002 is the official version to go along with that book.
    1.19  
    1.20 -The most prominent highlights of Isabelle2001 are as follows.  See the
    1.21 -NEWS file distributed with Isabelle for more details.
    1.22 +  * Explicit proof terms for Isabelle/Pure (Stefan Berghofer);
    1.23 +    all object-logics, proof tools etc. will automatically benefit.
    1.24 +
    1.25 +  * Interation of locales
    1.26  
    1.27 -  * Specific support for Poly/ML 4.1.1
    1.28 -    Faster, manages large heaps.
    1.29 +  * Specific support for Poly/ML 4.1.1 and PolyML/4.1.2
    1.30 +    (manage larger heaps, slightly faster).
    1.31  
    1.32 -  * Meta-level proof terms (Stefan Berghofer)
    1.33 +
    1.34  
    1.35 -You may get Isabelle2001 from any of the following mirror sites:
    1.36 +You may get Isabelle2002 from any of the following mirror sites:
    1.37  
    1.38    Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    1.39    Munich (Germany)  http://isabelle.in.tum.de/dist/