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.