[isabelle-dev] Towards localized syntax: bundle mixins for locale and class specifications – Discussion of alternatives

[Florian Haftmann]

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
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>>
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201127/d18035f1/attachment.sig>