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.
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