--- a/ANNOUNCE Wed Feb 27 15:23:42 2002 +0100
+++ b/ANNOUNCE Wed Feb 27 18:41:28 2002 +0100
@@ -4,20 +4,27 @@
Isabelle2002 is now available.
-This release clarifies long-standing issues at large, providing of
-more comfortable and robust environment.
+In this release many important aspects of Isabelle have been reworked
+to improve robustness and usability (this occasionally causes
+incompatibility with earlier versions).
-In this release a lot of important issues of existing concepts
+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;
+ Isabelle2002 is the official version to go along with that book.
-The most prominent highlights of Isabelle2001 are as follows. See the
-NEWS file distributed with Isabelle for more details.
+ * Explicit proof terms for Isabelle/Pure (Stefan Berghofer);
+ all object-logics, proof tools etc. will automatically benefit.
+
+ * Interation of locales
- * Specific support for Poly/ML 4.1.1
- Faster, manages large heaps.
+ * Specific support for Poly/ML 4.1.1 and PolyML/4.1.2
+ (manage larger heaps, slightly faster).
- * Meta-level proof terms (Stefan Berghofer)
+
-You may get Isabelle2001 from any of the following mirror sites:
+You may get Isabelle2002 from any of the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
Munich (Germany) http://isabelle.in.tum.de/dist/