equal
deleted
inserted
replaced
236 |
236 |
237 * Pure: syntax "CONST name" produces a fully internalized constant |
237 * Pure: syntax "CONST name" produces a fully internalized constant |
238 according to the current context. This is particularly useful for |
238 according to the current context. This is particularly useful for |
239 syntax translations that should refer to internal constant |
239 syntax translations that should refer to internal constant |
240 representations independently of name spaces. |
240 representations independently of name spaces. |
|
241 |
|
242 * Pure: syntax constant for foo (binder "FOO ") is called "foo_binder" |
|
243 instead of "FOO ". This allows multiple binder declarations to coexist |
|
244 in the same context. INCOMPATIBILITY. |
241 |
245 |
242 * Isar/locales: 'notation' provides a robust interface to the 'syntax' |
246 * Isar/locales: 'notation' provides a robust interface to the 'syntax' |
243 primitive that also works in a locale context (both for constants and |
247 primitive that also works in a locale context (both for constants and |
244 fixed variables). Type declaration and internal syntactic |
248 fixed variables). Type declaration and internal syntactic |
245 representation of given constants retrieved from the context. |
249 representation of given constants retrieved from the context. |