[isabelle-dev] Locale morphisms

[Clemens Ballarin]

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

This will be helpful especially in applications where locales have more 
than just a handful of parameters.

I'm mainly writing to find out whether the new keywords 'morphism' and 
'under' would be considered appropriate in the current framework of 
Isabelle's outer syntax.

Clemens