# HG changeset patch # User wenzelm # Date 1010705260 -3600 # Node ID 4013be8572c5b12ba1951046ce58484e0e477965 # Parent 05fa6a8a6320842bd4e73cacd1fbb2b6e7f11f6d * Pure: localized 'lemmas', 'theorems', 'declare'; diff -r 05fa6a8a6320 -r 4013be8572c5 NEWS --- 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;