Email Gateway (Nov 01 2020 at 16:52): Email Gateway (Nov 01 2020 at 16:52):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,
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
context
includes bundles
begin
…
end
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
follows:
locale / class foo = import +
includes bundles
fixes …
assumes …
begin
…
end
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
extended:
context foo
includes bundles
begin
…
end
This is effectively equal to
context foo
begin
context
includes bundles
begin
…
end
end
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
thread.
Cheers,
Florian
signature.asc
Email Gateway (Nov 01 2020 at 17:09):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,
currently the syntax for bundle mixins for locale / class specifications
looks as follows:
locale / class foo = import +
includes bundles
fixes …
assumes …
begin
…
end
While this use of »includes« rests firmly on established traditions, it
is a little bit unsatisfactory since it also applies to the »import«
expression, but is notated after it.
I had thought about something like
context
includes bundles
begin
locale foo = import +
fixes …
assumes …
begin
…
end
end
instead but this would require an artificial construction identifying
nested contexts as »morally being global« internally.
A more inspiring solution could be to abandon the existing »includes«
syntax entirely and replace it by a specific toplevel construct, e.g.
including bundles lemma foo: ‹…› if ‹…› for …
including bundles context group
begin
…
end
including bundles locale bar = …
This looks charming but the progressive participle is reserved for
proofs. For the same reason »with« won't do.
Cheers,
Florian
signature.asc
Last updated: Sep 26 2026 at 04:05 UTC