Re: [isabelle] [isabelle-dev] Locale interpretation introduces abbreviations rather than definitions



Am 17/07/2012 19:08, schrieb Florian Haftmann:
> Hi Peter,
> 
>> Currently, I am defining those constants by hand, after the
>> interpretation, which causes lots of boilerplate in my real applications
>> with more than a dozen of definitions.
> 
> the code generation tutorial gives a recommendation for that application
> (search for »interpretation« there).  There is also the theory
> »Interpretation_with_Defs« in src/HOL/ex for a experimental workaround.

Interpretation_with_Defs works well for me, I use it repeatedly in session IMP.

Tobias

> The discussion what interpretation could and should do with definitions
> stemming from locales is still ongoing (also sporadically on the mailing
> list), but I myself must reconsider the whole matter again first before
> I enter the discussion again.
> 
> Cheers,
> 	Florian
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.