[isabelle-dev] HOL/ex/Set_Algebras

[Clemens Ballarin]

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