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

Makarius 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
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


More information about the isabelle-dev mailing list