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 high-level proof |
87 version by Florian Kammüller, Isar locales package high-level 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 type-inference 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 ad-hoc 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 ad-hoc 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 meta-level 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 object-logic embedding (used by several tools internally); no longer |
|
116 use hard-wired "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 |