[isabelle-dev] HOL/ex/Set_Algebras

Clemens Ballarin ballarin at in.tum.de
Wed Apr 18 21:53:27 CEST 2012

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?


More information about the isabelle-dev mailing list