equal
deleted
inserted
replaced
254 Interpretation in locales only permits parameter renaming through the |
254 Interpretation in locales only permits parameter renaming through the |
255 locale expression. Interpretation is smart in that interpretations |
255 locale expression. Interpretation is smart in that interpretations |
256 that are active already do not occur in proof obligations, neither are |
256 that are active already do not occur in proof obligations, neither are |
257 instantiated theorems stored in duplicate. Use 'print_interps' to |
257 instantiated theorems stored in duplicate. Use 'print_interps' to |
258 inspect active interpretations of a particular locale. For details, |
258 inspect active interpretations of a particular locale. For details, |
259 see the Isar Reference manual. |
259 see the Isar Reference manual. Examples can be found in |
|
260 HOL/Finite_Set.thy and HOL/Algebra/UnivPoly.thy. |
260 |
261 |
261 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use |
262 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use |
262 'interpret' instead. |
263 'interpret' instead. |
263 |
264 |
264 * New context element 'constrains' for adding type constraints to |
265 * New context element 'constrains' for adding type constraints to |