[isabelle-dev] NEWS: Localized commands 'syntax' and 'no_syntax'
makarius at sketis.net
Wed Sep 22 12:20:19 CEST 2021
*** 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
This refers to Isabelle/eb54c0604ca5.
The idea has been in the pipeline for quite some time, and is now properly
materialized. The approach is rather basic: raw syntax refers to
global/extra-logical things and does not participate in transformation via
More information about the isabelle-dev