more stuff;
authorwenzelm
Thu Feb 28 21:30:03 2002 +0100 (2002-02-28)
changeset 129837d13480ee668
parent 12982 34a07757634d
child 12984 6071200efbf6
more stuff;
ANNOUNCE
     1.1 --- a/ANNOUNCE	Thu Feb 28 19:24:00 2002 +0100
     1.2 +++ b/ANNOUNCE	Thu Feb 28 21:30:03 2002 +0100
     1.3 @@ -4,24 +4,59 @@
     1.4  
     1.5  Isabelle2002 is now available.
     1.6  
     1.7 -In this release many important aspects of Isabelle have been reworked
     1.8 -to improve robustness and usability (this occasionally causes
     1.9 -incompatibility with earlier versions).
    1.10 +In this release many important aspects of Isabelle have been reworked,
    1.11 +to improve robustness and usability.  This occasionally causes
    1.12 +incompatibility with earlier versions.
    1.13  
    1.14 -The most prominent highlights of Isabelle2002 are as follows; see the
    1.15 -NEWS of the distribution for more details.
    1.16 +The most prominent highlights of Isabelle2002 are as follows (see the
    1.17 +NEWS of the distribution for more details).
    1.18  
    1.19    * The Isabelle/HOL tutorial has been published as LNCS 2283;
    1.20 -    Isabelle2002 is the official version to go along with that book.
    1.21 +    Isabelle2002 is the official version to go along with that book
    1.22 +    (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
    1.23 +
    1.24 +  * Pure: explicit proof terms for all internal inferences:
    1.25 +    object-logics, proof tools etc. will benefit automatically
    1.26 +    (by Stefan Berghofer).
    1.27  
    1.28 -  * Explicit proof terms for Isabelle/Pure (Stefan Berghofer);
    1.29 -    all object-logics, proof tools etc. will automatically benefit.
    1.30 +  * Pure/Isar: proper integration of the locale package for modular
    1.31 +    theory development; additional support for rename/merge
    1.32 +    operations, and type-inference for structured specifications
    1.33 +    (by Markus Wenzel).
    1.34 +
    1.35 +  * Pure/Isar: streamlined induction proof patterns
    1.36 +    (by Markus Wenzel).
    1.37 +
    1.38 +  * Pure/HOL: infrastructure for generating functional and relational
    1.39 +    code, using the ML run-time environment (by Stefan Berghofer).
    1.40 +
    1.41 +  * HOL/library: sane numerals on all number types; several
    1.42 +    improvements of tuple and record types; new definite description
    1.43 +    operator; keep Hilbert's choice out of basic theories.
    1.44  
    1.45 -  * Interation of locales
    1.46 +  * HOL/Bali: large application concerning formal treatment of Java.
    1.47 +    (by David von Oheimb and Norbert Schirmer).
    1.48 +
    1.49 +  * HOL/Hoare_Parallel: large application concerning verification of
    1.50 +    parallel imperative programs (Owicki-Gries method etc.)
    1.51 +    (by Leonor Prensa Nieto).
    1.52 +
    1.53 +  * HOL/GroupTheory: group theory examples including Sylow's theorem
    1.54 +    (by Florian Kammüller).
    1.55  
    1.56 -  * Specific support for Poly/ML 4.1.1 and PolyML/4.1.2
    1.57 -    (manage larger heaps, slightly faster).
    1.58 +  * HOL/IMP: new proofs in Isar format
    1.59 +    (by Gerwin Klein).
    1.60 +
    1.61 +  * ZF/UNITY: typeless version of Chandy and Misra's formalism
    1.62 +    (by Sidi O Ehmety).
    1.63  
    1.64 +  * System: improvements and simplifications of document preparation
    1.65 +    (by Markus Wenzel).
    1.66 +
    1.67 +  * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
    1.68 +    larger heap size of applications.
    1.69 +
    1.70 +  * System: support for MacOS X (for Poly/ML and SML/NJ).
    1.71  
    1.72  
    1.73  You may get Isabelle2002 from any of the following mirror sites: