Re: [isabelle] making local definitions programmatically

Florian Haftmann wrote:

> I must confess the qualification conventions appear to me also a
> little bit obscure.  Generally, most times it is preferable to store
> the logical entities stemming from definitions etc. in separate
> tables for later usage.

Dear Florian,

Thanks for your help with this; my code now works.

As for this last point, I thought that I would do as you suggest (keep
track of what is returned by LocalTheory.define), but if you check
what it does, you don't actually get a Const back.  Instead, the term
returned is a Free, with an unqualified name.

So this doesn't seem to be so helpful. (Perhaps I could take the defining theorem apart....)


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