ballarin at in.tum.de
Wed Apr 18 21:53:27 CEST 2012
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?
More information about the isabelle-dev