[isabelle-dev] NEWS: Localized commands 'syntax' and 'no_syntax'

[Makarius]

*** 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.

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
morphisms.


	Makarius