lcp's try
Fri, 01 Mar 2002 13:07:25 +0100
changeset 12993 1b76cc7ffef7
parent 12992 c2648d3e67a8
child 12994 e5d3cdba117e
lcp's try
--- 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).