ANNOUNCE
changeset 12993 1b76cc7ffef7
parent 12983 7d13480ee668
child 12995 d9da3015aab4
     1.1 --- a/ANNOUNCE	Fri Mar 01 11:55:45 2002 +0100
     1.2 +++ b/ANNOUNCE	Fri Mar 01 13:07:25 2002 +0100
     1.3 @@ -4,8 +4,9 @@
     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 +This release provides major improvements.  The Isar language has reached a
    1.10 +mature state; the treatment of numerals has been streamlined; several
    1.11 +substantial case studies have been added.  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 @@ -30,9 +31,9 @@
    1.16    * Pure/HOL: infrastructure for generating functional and relational
    1.17      code, using the ML run-time environment (by Stefan Berghofer).
    1.18  
    1.19 -  * HOL/library: sane numerals on all number types; several
    1.20 +  * HOL/library: numerals on all number types; several
    1.21      improvements of tuple and record types; new definite description
    1.22 -    operator; keep Hilbert's choice out of basic theories.
    1.23 +    operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
    1.24  
    1.25    * HOL/Bali: large application concerning formal treatment of Java.
    1.26      (by David von Oheimb and Norbert Schirmer).