1.1 --- a/NEWS	Tue Nov 06 23:47:35 2001 +0100
     1.2 +++ b/NEWS	Tue Nov 06 23:50:24 2001 +0100
     1.3 @@ -62,6 +62,15 @@
     1.4  statements; NB: major inductive premises need to be put first, all the
     1.5  rest of the goal is passed through the induction;
     1.6  
     1.7 +* Pure: proper integration with ``locales''; unlike the original
     1.8 +version by Florian Kammueller, Isar locales package high-level proof
     1.9 +contexts rather than raw logical ones (e.g. we admit to include
    1.10 +attributes everywhere);
    1.11 +
    1.12 +* Pure: theory goals now support ad-hoc contexts, which are discharged
    1.13 +in the result, as in ``lemma (assumes A and B) K: A .''; syntax
    1.14 +coincides with that of a locale body;
    1.15 +
    1.16  * Pure: renamed "antecedent" case to "rule_context";
    1.17  
    1.18  * Pure: added 'corollary' command;