Re: [isabelle] theory_of_thm @{thm xxx}

On Wed, 22 Aug 2012, Peter Lammich wrote:

However, just introducing this (artificial, and on first glance unnecessary) dependence might be the quickest way to solve the problem.

The cleanest (?) might be to manually transfer the theorems extracted from the record type to the theory of the theorem that is passed to the attribute (This theory should always include both, the theory of the record type and the one declaring the attribute)

I can only guess what your overall structure is, but the latter also sounds right to me. The function for that is Thm.transfer.


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