Hi Florian,
Could you please explain what you mean by "surface context" in the
documentation of the locale command:
given bundles take effect in the surface context within both import and
body and the potentially following begin / end block
I'm trying to understand where exactly bundles in locale declarations
are effective. I suppose they are not persisted beyond the locale
declaration's begin /end block?
Clemens
On 2020-11-27 18:46, Florian Haftmann wrote:
See now http://isabelle.in.tum.de/repos/isabelle/rev/e7c2848b78e8 for a
refined and documented version.
Florian
Am 21.11.20 um 09:01 schrieb Florian Haftmann:
Since this thread did not stimulate any activity I will go on to
document the syntax in NEWS entries and manuals.
Cheers,
Florian
Am 01.11.20 um 18:09 schrieb Florian Haftmann:
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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
