1.1 --- a/ANNOUNCE	Wed Feb 27 15:23:42 2002 +0100
     1.2 +++ b/ANNOUNCE	Wed Feb 27 18:41:28 2002 +0100
     1.3 @@ -4,20 +4,27 @@
     1.4  
     1.5  Isabelle2002 is now available.
     1.6  
     1.7 -This release clarifies long-standing issues at large, providing of
     1.8 -more comfortable and robust environment.
     1.9 +In this release many important aspects of Isabelle have been reworked
    1.10 +to improve robustness and usability (this occasionally causes
    1.11 +incompatibility with earlier versions).
    1.12  
    1.13 -In this release a lot of important issues of existing concepts 
    1.14 +The most prominent highlights of Isabelle2002 are as follows; see the
    1.15 +NEWS of the distribution for more details.
    1.16  
    1.17 -The most prominent highlights of Isabelle2001 are as follows.  See the
    1.18 -NEWS file distributed with Isabelle for more details.
    1.19 +  * The Isabelle/HOL tutorial has been published as LNCS 2283;
    1.20 +    Isabelle2002 is the official version to go along with that book.
    1.21  
    1.22 -  * Specific support for Poly/ML 4.1.1
    1.23 -    Faster, manages large heaps.
    1.24 +  * Explicit proof terms for Isabelle/Pure (Stefan Berghofer);
    1.25 +    all object-logics, proof tools etc. will automatically benefit.
    1.26  
    1.27 -  * Meta-level proof terms (Stefan Berghofer)
    1.28 +  * Interation of locales
    1.29  
    1.30 -You may get Isabelle2001 from any of the following mirror sites:
    1.31 +  * Specific support for Poly/ML 4.1.1 and PolyML/4.1.2
    1.32 +    (manage larger heaps, slightly faster).
    1.33 +
    1.34 +
    1.35 +
    1.36 +You may get Isabelle2002 from any of the following mirror sites:
    1.37  
    1.38    Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    1.39    Munich (Germany)  http://isabelle.in.tum.de/dist/

     2.1 --- a/NEWS	Wed Feb 27 15:23:42 2002 +0100
     2.2 +++ b/NEWS	Wed Feb 27 18:41:28 2002 +0100
     2.3 @@ -87,7 +87,9 @@
     2.4  version by Florian Kammüller, Isar locales package high-level proof
     2.5  contexts rather than raw logical ones (e.g. we admit to include
     2.6  attributes everywhere); operations on locales include merge and
     2.7 -rename; e.g. see HOL/ex/Locales.thy;
     2.8 +rename; support for implicit arguments (``structures''); simultaneous
     2.9 +type-inference over imports and text; see also HOL/ex/Locales.thy for
    2.10 +some examples;
    2.11  
    2.12  * Pure: the following commands have been ``localized'', supporting a
    2.13  target locale specification "(in name)": 'lemma', 'theorem',
    2.14 @@ -95,12 +97,24 @@
    2.15  stored both within the locale and at the theory level (exported and
    2.16  qualified by the locale name);
    2.17  
    2.18 -* Pure: theory goals now support ad-hoc contexts, which are discharged
    2.19 -in the result, as in ``lemma (assumes A and B) K: A .''; syntax
    2.20 -coincides with that of a locale body;
    2.21 +* Pure: theory goals may now be specified in ``long'' form, with
    2.22 +ad-hoc contexts consisting of arbitrary locale elements. for example
    2.23 +``lemma foo: fixes x assumes "A x" shows "B x"'' (local syntax and
    2.24 +definitions may be given, too); the result is a meta-level rule with
    2.25 +the context elements being discharged in the obvious way;
    2.26 +
    2.27 +* Pure: new proof command 'using' allows to augment currently used
    2.28 +facts after a goal statement ('using' is syntactically analogous to
    2.29 +'apply', but acts on the goal's facts only); this allows chained facts
    2.30 +to be separated into parts given before and after a claim, as in
    2.31 +``from a and b have C using d and e <proof>'';
    2.32  
    2.33  * Pure: renamed "antecedent" case to "rule_context";
    2.34  
    2.35 +* Pure: new 'judgment' command records explicit information about the
    2.36 +object-logic embedding (used by several tools internally); no longer
    2.37 +use hard-wired "Trueprop";
    2.38 +
    2.39  * Pure: added 'corollary' command;
    2.40  
    2.41  * Pure: fixed 'token_translation' command;