# HG changeset patch
# User wenzelm
# Date 1014988303 -3600
# Node ID d9da3015aab4e166790483ceb68fe3405ec9443d
# Parent  e5d3cdba117e1fac48ba6cc4ca38e8845955bae1
tuned;

diff -r e5d3cdba117e -r d9da3015aab4 ANNOUNCE
--- a/ANNOUNCE	Fri Mar 01 13:23:10 2002 +0100
+++ b/ANNOUNCE	Fri Mar 01 14:11:43 2002 +0100
@@ -4,15 +4,17 @@
 
 Isabelle2002 is now available.
 
-This release provides major improvements.  The Isar language has reached a
-mature state; the treatment of numerals has been streamlined; several
-substantial case studies have been added.  This occasionally causes
-incompatibility with earlier versions.
+This release provides major improvements.  The Isar language has
+reached a mature state; the core engine is able to record full proof
+terms; many aspects of the library have been reworked; several
+substantial case studies have been added.  Some changes may cause
+incompatibility with earlier versions, but improve accessibility of
+Isabelle for new users.
 
 The most prominent highlights of Isabelle2002 are as follows (see the
 NEWS of the distribution for more details).
 
-  * The Isabelle/HOL tutorial has been published as LNCS 2283;
+  * The Isabelle/HOL tutorial is to be published as LNCS 2283;
     Isabelle2002 is the official version to go along with that book
     (by Tobias Nipkow, Larry Paulson, Markus Wenzel).