[isabelle-dev] Locale morphisms

[Gerwin Klein]

> On 8 Jan 2022, at 01:37, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> On 07/01/2022 15:12, Clemens Ballarin wrote:
>> Dear Isabelle Developers,
>> I'm working on an extension of the locale machinery by a means of declaring morphisms for use in locale expressions. Currently morphisms only appear within locale expressions. For example, in
>>   interpretation my_locale where A = t and B = s
>> the parameters A and B of 'my_locale' are mapped to t and s from the current context. The extension would introduce a new command 'morphism' for declaring morphisms and a new keyword 'under' for referring to these morphisms in expressions:
>>   morphism my_morphism where A = t and B = s
>>   interpretation my_locale under my_morphism
> 
> I wonder if "with" could be reused instead?

I'd second that.

Cheers,
Gerwin
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220107/208d05e9/attachment.sig>