1.1 --- a/NEWS	Thu Jan 10 21:04:15 2002 +0100
     1.2 +++ b/NEWS	Fri Jan 11 00:27:40 2002 +0100
     1.3 @@ -83,6 +83,12 @@
     1.4  attributes everywhere); operations on locales include merge and
     1.5  rename; e.g. see HOL/ex/Locales.thy;
     1.6  
     1.7 +* Pure: the following commands have been ``localized'', supporting a
     1.8 +target locale specification "(in name)": 'lemma', 'theorem',
     1.9 +'corollary', 'lemmas', 'theorems', 'declare'; the results will be
    1.10 +stored both within the locale and at the theory level (exported and
    1.11 +qualified by the locale name);
    1.12 +
    1.13  * Pure: theory goals now support ad-hoc contexts, which are discharged
    1.14  in the result, as in ``lemma (assumes A and B) K: A .''; syntax
    1.15  coincides with that of a locale body;