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