* Pure: localized 'lemmas', 'theorems', 'declare';
Fri, 11 Jan 2002 00:27:40 +0100
changeset 12707 4013be8572c5
parent 12706 05fa6a8a6320
child 12708 31672377dadc
* Pure: localized 'lemmas', 'theorems', 'declare';
--- a/NEWS	Thu Jan 10 21:04:15 2002 +0100
+++ b/NEWS	Fri Jan 11 00:27:40 2002 +0100
@@ -83,6 +83,12 @@
 attributes everywhere); operations on locales include merge and
 rename; e.g. see HOL/ex/Locales.thy;
+* Pure: the following commands have been ``localized'', supporting a
+target locale specification "(in name)": 'lemma', 'theorem',
+'corollary', 'lemmas', 'theorems', 'declare'; the results will be
+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;