369 instead of "FOO ". This allows multiple binder declarations to coexist |
369 instead of "FOO ". This allows multiple binder declarations to coexist |
370 in the same context. INCOMPATIBILITY. |
370 in the same context. INCOMPATIBILITY. |
371 |
371 |
372 * Isar/locales: 'notation' provides a robust interface to the 'syntax' |
372 * Isar/locales: 'notation' provides a robust interface to the 'syntax' |
373 primitive that also works in a locale context (both for constants and |
373 primitive that also works in a locale context (both for constants and |
374 fixed variables). Type declaration and internal syntactic |
374 fixed variables). Type declaration and internal syntactic representation |
375 representation of given constants retrieved from the context. |
375 of given constants retrieved from the context. Likewise, the |
|
376 'no_notation' command allows to remove given syntax annotations from the |
|
377 current context. |
376 |
378 |
377 * Isar/locales: new derived specification elements 'axiomatization', |
379 * Isar/locales: new derived specification elements 'axiomatization', |
378 'definition', 'abbreviation', which support type-inference, admit |
380 'definition', 'abbreviation', which support type-inference, admit |
379 object-level specifications (equality, equivalence). See also the |
381 object-level specifications (equality, equivalence). See also the |
380 isar-ref manual. Examples: |
382 isar-ref manual. Examples: |