# HG changeset patch
# User wenzelm
# Date 1014831688 -3600
# Node ID 2ac9265b2cd53fd510f3255b675805cff220c8e8
# Parent  73fb6a200e3610b88e9361871d970f8593e09cd2
tuned;

diff -r 73fb6a200e36 -r 2ac9265b2cd5 ANNOUNCE
--- 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/
diff -r 73fb6a200e36 -r 2ac9265b2cd5 NEWS
--- a/NEWS	Wed Feb 27 15:23:42 2002 +0100
+++ b/NEWS	Wed Feb 27 18:41:28 2002 +0100
@@ -87,7 +87,9 @@
 version by Florian Kammüller, Isar locales package high-level proof
 contexts rather than raw logical ones (e.g. we admit to include
 attributes everywhere); operations on locales include merge and
-rename; e.g. see HOL/ex/Locales.thy;
+rename; support for implicit arguments (``structures''); simultaneous
+type-inference over imports and text; see also HOL/ex/Locales.thy for
+some examples;
 
 * Pure: the following commands have been ``localized'', supporting a
 target locale specification "(in name)": 'lemma', 'theorem',
@@ -95,12 +97,24 @@
 stored both within the locale and at the theory level (exported and
 qualified by the locale name);
 
-* Pure: theory goals now support ad-hoc contexts, which are discharged
-in the result, as in ``lemma (assumes A and B) K: A .''; syntax
-coincides with that of a locale body;
+* Pure: theory goals may now be specified in ``long'' form, with
+ad-hoc contexts consisting of arbitrary locale elements. for example
+``lemma foo: fixes x assumes "A x" shows "B x"'' (local syntax and
+definitions may be given, too); the result is a meta-level rule with
+the context elements being discharged in the obvious way;
+
+* Pure: new proof command 'using' allows to augment currently used
+facts after a goal statement ('using' is syntactically analogous to
+'apply', but acts on the goal's facts only); this allows chained facts
+to be separated into parts given before and after a claim, as in
+``from a and b have C using d and e <proof>'';
 
 * Pure: renamed "antecedent" case to "rule_context";
 
+* Pure: new 'judgment' command records explicit information about the
+object-logic embedding (used by several tools internally); no longer
+use hard-wired "Trueprop";
+
 * Pure: added 'corollary' command;
 
 * Pure: fixed 'token_translation' command;