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

On 07/17/2012 07:08 PM, Florian Haftmann wrote:
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.
In our ITP 2011 paper, Andreas and I suggest an alternative approach that allows code generation from locale definitions more easily than the recommendation in the code generation tutorial.


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