changeset 11600 bbd6268e0b4b
parent 11109 ce1cefc6c14c
child 12927 b7c916bf3332
--- a/ANNOUNCE	Thu Sep 27 18:46:32 2001 +0200
+++ b/ANNOUNCE	Thu Sep 27 18:56:39 2001 +0200
@@ -1,43 +1,18 @@
-Subject: Announcing Isabelle99-2
+Subject: Announcing Isabelle2001
-Isabelle99-2 is now available.  This release continues the line of
-Isabelle99, introducing various improvements in robustness and
+Isabelle2001 is now available.
-The most prominent highlights of Isabelle99-2 are as follows.  See the
+The most prominent highlights of Isabelle2001 are as follows.  See the
 NEWS file distributed with Isabelle for more details.
-  * Poly/ML 4.0 used by default
-    More robust, less disk space required.
-  * Simplifier (Stefan Berghofer)
-    Proper implementation as a derived rule, outside the kernel!
-  * Improved document preparation (Markus Wenzel)
-    Near math-mode, sub/super scripts, more symbols etc.
-  * Isabelle/Isar (Markus Wenzel)
-    Numerous usability improvements, e.g. support for initial
-    schematic goals, failure prediction of subgoal statements,
-    handling of non-atomic statements in induction.
+  * Specific support for Poly/ML 4.1.1
+    Faster, manages large heaps.
-  * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
-      Thomas M Rasmussen, Markus Wenzel)
-    A collection of generic theories to be used together with main HOL.
-  * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
-    General cleanup, more on nonstandard real analysis.
+  * Meta-level proof terms (Stefan Berghofer)
-  * HOL/Unix (Markus Wenzel)
-    Some Aspects of Unix file-system security; demonstrates
-    Isabelle/Isar in typical system modelling and verification tasks.
-  * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
-    Extended version of the Isabelle/HOL tutorial.
-You may get Isabelle99-2 from any of the following mirror sites:
+You may get Isabelle2001 from any of the following mirror sites:
   Cambridge (UK)
   Munich (Germany)