Hi Florian,
Thanks for the clarification.
Its purpose
might have been to make the interpretation notationally simpler.
the story behind is not about syntax. It is really about the
simultaneous definitions. For a motivation, you can have a look at the
tutorial on code generation, section »Further issues«, »Locales and
interpretation«, where the pattern behind interpretation plus definition
is spelt out using the constant »funpows«.
This looks to me like a special case, but maybe one that is
encountered frequently when generating code. What do you intend to
do? Provide a special version of interpretation for code generation?
Clemens
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
