ANNOUNCE
changeset 12995 d9da3015aab4
parent 12993 1b76cc7ffef7
child 12996 7ac0a7e306db
     1.1 --- a/ANNOUNCE	Fri Mar 01 13:23:10 2002 +0100
     1.2 +++ b/ANNOUNCE	Fri Mar 01 14:11:43 2002 +0100
     1.3 @@ -4,15 +4,17 @@
     1.4  
     1.5  Isabelle2002 is now available.
     1.6  
     1.7 -This release provides major improvements.  The Isar language has reached a
     1.8 -mature state; the treatment of numerals has been streamlined; several
     1.9 -substantial case studies have been added.  This occasionally causes
    1.10 -incompatibility with earlier versions.
    1.11 +This release provides major improvements.  The Isar language has
    1.12 +reached a mature state; the core engine is able to record full proof
    1.13 +terms; many aspects of the library have been reworked; several
    1.14 +substantial case studies have been added.  Some changes may cause
    1.15 +incompatibility with earlier versions, but improve accessibility of
    1.16 +Isabelle for new users.
    1.17  
    1.18  The most prominent highlights of Isabelle2002 are as follows (see the
    1.19  NEWS of the distribution for more details).
    1.20  
    1.21 -  * The Isabelle/HOL tutorial has been published as LNCS 2283;
    1.22 +  * The Isabelle/HOL tutorial is to be published as LNCS 2283;
    1.23      Isabelle2002 is the official version to go along with that book
    1.24      (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
    1.25