equal
deleted
inserted
replaced
161 the instantiated theorems of the locale are added to the theory or proof |
161 the instantiated theorems of the locale are added to the theory or proof |
162 context. Interpretation is smart in that already active interpretations |
162 context. Interpretation is smart in that already active interpretations |
163 do not occur in proof obligations, neither are instantiated theorems stored |
163 do not occur in proof obligations, neither are instantiated theorems stored |
164 in duplicate. |
164 in duplicate. |
165 Use print_interps to inspect active interpretations of a particular locale. |
165 Use print_interps to inspect active interpretations of a particular locale. |
|
166 For details, see the Isar Reference manual. |
166 |
167 |
167 * Locales: proper static binding of attribute syntax -- i.e. types / |
168 * Locales: proper static binding of attribute syntax -- i.e. types / |
168 terms / facts mentioned as arguments are always those of the locale |
169 terms / facts mentioned as arguments are always those of the locale |
169 definition context, independently of the context of later |
170 definition context, independently of the context of later |
170 invocations. Moreover, locale operations (renaming and type / term |
171 invocations. Moreover, locale operations (renaming and type / term |