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

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.

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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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