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
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
