[isabelle-dev] Towards localized syntax: bundle mixins for locale and class specifications
florian.haftmann at informatik.tu-muenchen.de
Sun Nov 1 17:52:09 CET 2020
my recent re-working of parts of the local theory infrastructure has
inspired me to close a long-standing gap in our module system: the
ability to organize syntax declarations into bundles and use them in
confined nested blocks
so far did not extend to class and locale specifications, which by their
very nature are always given at the outermost specification layer.
Taking the existing »includes« syntax as a base, the result looks as
locale / class foo = import +
The declarations from the given bundle(s) are active for the locale /
class specification itself and the optional following context block.
For consistency, also the syntax for re-opening of named contexts is
This is effectively equal to
See src/HOL/ex/Specifications_with_bundle_mixins.thy for examples.
This refers to rev. 589645894305.
NEWS entries and documentation updates have still to be written, but I
want to discuss possible alternative syntactic notations in a separate
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev