# HG changeset patch
# User paulson
# Date 1014984445 -3600
# Node ID 1b76cc7ffef70a0d5aa58a777c0301cd5e3a0a76
# Parent  c2648d3e67a85c97243ef79dccc9bfdfbfbe9643
lcp's try

diff -r c2648d3e67a8 -r 1b76cc7ffef7 ANNOUNCE
--- a/ANNOUNCE	Fri Mar 01 11:55:45 2002 +0100
+++ b/ANNOUNCE	Fri Mar 01 13:07:25 2002 +0100
@@ -4,8 +4,9 @@
 
 Isabelle2002 is now available.
 
-In this release many important aspects of Isabelle have been reworked,
-to improve robustness and usability.  This occasionally causes
+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.
 
 The most prominent highlights of Isabelle2002 are as follows (see the
@@ -30,9 +31,9 @@
   * Pure/HOL: infrastructure for generating functional and relational
     code, using the ML run-time environment (by Stefan Berghofer).
 
-  * HOL/library: sane numerals on all number types; several
+  * HOL/library: numerals on all number types; several
     improvements of tuple and record types; new definite description
-    operator; keep Hilbert's choice out of basic theories.
+    operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
 
   * HOL/Bali: large application concerning formal treatment of Java.
     (by David von Oheimb and Norbert Schirmer).