85 
85 
86 * Pure: proper integration with ``locales''; unlike the original 
86 * Pure: proper integration with ``locales''; unlike the original 
87 version by Florian Kammüller, Isar locales package highlevel proof 
87 version by Florian Kammüller, Isar locales package highlevel proof 
88 contexts rather than raw logical ones (e.g. we admit to include 
88 contexts rather than raw logical ones (e.g. we admit to include 
89 attributes everywhere); operations on locales include merge and 
89 attributes everywhere); operations on locales include merge and 
90 rename; e.g. see HOL/ex/Locales.thy; 
90 rename; support for implicit arguments (``structures''); simultaneous 

91 typeinference over imports and text; see also HOL/ex/Locales.thy for 

92 some examples; 
91 
93 
92 * Pure: the following commands have been ``localized'', supporting a 
94 * Pure: the following commands have been ``localized'', supporting a 
93 target locale specification "(in name)": 'lemma', 'theorem', 
95 target locale specification "(in name)": 'lemma', 'theorem', 
94 'corollary', 'lemmas', 'theorems', 'declare'; the results will be 
96 'corollary', 'lemmas', 'theorems', 'declare'; the results will be 
95 stored both within the locale and at the theory level (exported and 
97 stored both within the locale and at the theory level (exported and 
96 qualified by the locale name); 
98 qualified by the locale name); 
97 
99 
98 * Pure: theory goals now support adhoc contexts, which are discharged 
100 * Pure: theory goals may now be specified in ``long'' form, with 
99 in the result, as in ``lemma (assumes A and B) K: A .''; syntax 
101 adhoc contexts consisting of arbitrary locale elements. for example 
100 coincides with that of a locale body; 
102 ``lemma foo: fixes x assumes "A x" shows "B x"'' (local syntax and 

103 definitions may be given, too); the result is a metalevel rule with 

104 the context elements being discharged in the obvious way; 

105 

106 * Pure: new proof command 'using' allows to augment currently used 

107 facts after a goal statement ('using' is syntactically analogous to 

108 'apply', but acts on the goal's facts only); this allows chained facts 

109 to be separated into parts given before and after a claim, as in 

110 ``from a and b have C using d and e <proof>''; 
101 
111 
102 * Pure: renamed "antecedent" case to "rule_context"; 
112 * Pure: renamed "antecedent" case to "rule_context"; 

113 

114 * Pure: new 'judgment' command records explicit information about the 

115 objectlogic embedding (used by several tools internally); no longer 

116 use hardwired "Trueprop"; 
103 
117 
104 * Pure: added 'corollary' command; 
118 * Pure: added 'corollary' command; 
105 
119 
106 * Pure: fixed 'token_translation' command; 
120 * Pure: fixed 'token_translation' command; 
107 
121 