Re: [isabelle] [isabelle-dev] Locale interpretation introduces abbreviations rather than definitions
On 07/17/2012 07:08 PM, Florian Haftmann wrote:
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and