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