Re: [isabelle] theory_of_thm @{thm xxx}

On Wed, 22 Aug 2012, Peter Lammich wrote:

In my particular case, I have implemented an attribute that also uses theorems fetched from record types. The problem is, that the theory that declares the record type does not import the theory that declares the attribute.

For now, I solved the problem by fetching the theorems in their original context, and then transferring them to HOL/Main, assuming that all theorems that my attribute sees depend on a super-theory of Main, which is realistic in my case.

So why not make the imports right, according to what you do formally?


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