Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Localized commands 'syntax' and 'no_...

Email Gateway (Sep 22 2021 at 10:20):

From: Makarius <makarius@sketis.net>
* 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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Apr 20 2024 at 04:19 UTC