Re: [isabelle] theory_of_thm @{thm xxx}

On Mi, 2012-08-22 at 13:21 +0200, Makarius wrote:
> 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.

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

Because this is not the "right" way from a modularization standpoint.
The theory that declares the record type and the theory that declares
the attribute are independent, so I see no need to import the one from
the other. The dependence is established by a third theory, importing
both, and using the attribute declared in the latter with a theorem
containing the record type declared in the former.

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)


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