Localized commands 'syntax' and 'no_syntax'
General
- Commands syntax and no_syntax now work in a local theory context, but there is no proper way to refer to local entities --- in contrast to notation and no_notation. Local syntax works well with bundle, e.g. see lattice_syntax vs. no_lattice_syntax in theory Main of Isabelle/HOL.
This refers to Isabelle/eb54c0604ca5.
- Projects
- None
- Subscribers
- None