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