NEWS
changeset 12964 2ac9265b2cd5
parent 12924 02eb40cde931
child 12984 6071200efbf6
     1.1 --- a/NEWS	Wed Feb 27 15:23:42 2002 +0100
     1.2 +++ b/NEWS	Wed Feb 27 18:41:28 2002 +0100
     1.3 @@ -87,7 +87,9 @@
     1.4  version by Florian Kammüller, Isar locales package high-level proof
     1.5  contexts rather than raw logical ones (e.g. we admit to include
     1.6  attributes everywhere); operations on locales include merge and
     1.7 -rename; e.g. see HOL/ex/Locales.thy;
     1.8 +rename; support for implicit arguments (``structures''); simultaneous
     1.9 +type-inference over imports and text; see also HOL/ex/Locales.thy for
    1.10 +some examples;
    1.11  
    1.12  * Pure: the following commands have been ``localized'', supporting a
    1.13  target locale specification "(in name)": 'lemma', 'theorem',
    1.14 @@ -95,12 +97,24 @@
    1.15  stored both within the locale and at the theory level (exported and
    1.16  qualified by the locale name);
    1.17  
    1.18 -* Pure: theory goals now support ad-hoc contexts, which are discharged
    1.19 -in the result, as in ``lemma (assumes A and B) K: A .''; syntax
    1.20 -coincides with that of a locale body;
    1.21 +* Pure: theory goals may now be specified in ``long'' form, with
    1.22 +ad-hoc contexts consisting of arbitrary locale elements. for example
    1.23 +``lemma foo: fixes x assumes "A x" shows "B x"'' (local syntax and
    1.24 +definitions may be given, too); the result is a meta-level rule with
    1.25 +the context elements being discharged in the obvious way;
    1.26 +
    1.27 +* Pure: new proof command 'using' allows to augment currently used
    1.28 +facts after a goal statement ('using' is syntactically analogous to
    1.29 +'apply', but acts on the goal's facts only); this allows chained facts
    1.30 +to be separated into parts given before and after a claim, as in
    1.31 +``from a and b have C using d and e <proof>'';
    1.32  
    1.33  * Pure: renamed "antecedent" case to "rule_context";
    1.34  
    1.35 +* Pure: new 'judgment' command records explicit information about the
    1.36 +object-logic embedding (used by several tools internally); no longer
    1.37 +use hard-wired "Trueprop";
    1.38 +
    1.39  * Pure: added 'corollary' command;
    1.40  
    1.41  * Pure: fixed 'token_translation' command;