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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



Attachment: signature.asc
Description: OpenPGP digital signature



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