ANNOUNCE
changeset 13042 d8a345d9e067
parent 13010 3437d8d89803
child 13045 1db0bdda1d32
     1.1 --- a/ANNOUNCE	Mon Mar 04 14:27:10 2002 +0100
     1.2 +++ b/ANNOUNCE	Thu Mar 07 23:21:19 2002 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4      Isabelle2002 is the official version to go along with that book
     1.5      (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
     1.6  
     1.7 -  * Pure: explicit proof terms for all internal inferences:
     1.8 +  * Pure: explicit proof terms for all internal inferences;
     1.9      object-logics, proof tools etc. will benefit automatically
    1.10      (by Stefan Berghofer).
    1.11  
    1.12 @@ -27,28 +27,30 @@
    1.13      operations, and type-inference for structured specifications
    1.14      (by Markus Wenzel).
    1.15  
    1.16 -  * Pure/Isar: streamlined induction proof patterns
    1.17 +  * Pure/Isar: streamlined cases/induction proof patterns
    1.18      (by Markus Wenzel).
    1.19  
    1.20    * Pure/HOL: infrastructure for generating functional and relational
    1.21 -    code, using the ML run-time environment (by Stefan Berghofer).
    1.22 +    code, using the ML run-time environment
    1.23 +    (by Stefan Berghofer).
    1.24  
    1.25 -  * HOL/library: numerals on all number types; several
    1.26 -    improvements of tuple and record types; new definite description
    1.27 -    operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
    1.28 +  * HOL/library: numerals on all number types; several improvements of
    1.29 +    tuple and record types; new definite description operator; keep
    1.30 +    Hilbert's epsilon (Axiom of Choice) out of basic theories
    1.31 +    (by Stefan Berghofer, Larry Paulson, Markus Wenzel).
    1.32  
    1.33    * HOL/Bali: large application concerning formal treatment of Java.
    1.34      (by David von Oheimb and Norbert Schirmer).
    1.35  
    1.36    * HOL/HoareParallel: large application concerning verification of
    1.37      parallel imperative programs (Owicki-Gries method, Rely-Guarantee
    1.38 -    method, examples of garbage collection, mutual exclusion, etc.)
    1.39 +    method, examples of garbage collection, mutual exclusion)
    1.40      (by Leonor Prensa Nieto).
    1.41  
    1.42    * HOL/GroupTheory: group theory examples including Sylow's theorem
    1.43 -    (by Florian Kammüller).
    1.44 +    (by Florian Kammueller).
    1.45  
    1.46 -  * HOL/IMP: new proofs in Isar format
    1.47 +  * HOL/IMP: several new proofs in Isar format
    1.48      (by Gerwin Klein).
    1.49  
    1.50    * HOL/MicroJava: exception handling on the bytecode level
    1.51 @@ -61,10 +63,8 @@
    1.52      (by Markus Wenzel).
    1.53  
    1.54    * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
    1.55 -    larger heap size of applications.
    1.56 -
    1.57 -  * System: support for MacOS X (for Poly/ML and SML/NJ).
    1.58 -
    1.59 +    larger heap size of applications; support for MacOS X (Poly/ML and
    1.60 +    SML/NJ).
    1.61  
    1.62  You may get Isabelle2002 from any of the following mirror sites:
    1.63