*** 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
