Re: [isabelle] theory_of_thm @{thm xxx}



On 22/08/12 21:19, Makarius wrote:
On Wed, 22 Aug 2012, Thomas Sewell wrote:

In principle, having @{thm meta_mp} live only in @{theory Pure} would make
perfect sense.
These problems are long forgotten, because the transfer principle is the
established way for such a long time already.  (This is in disagreement
with the very first sentence above.)

Apologies for nitpicking, but there is room for us both to be right. This might be a principled approach, and it has pragmatic merit and the weight of tradition, but, in principle, there might be other valid approaches.

For instance, a system like Isabelle could have theorems depend on lists of theories, or equivalently construct meet/join objects in the theory lattice. It would probably be inefficient and sometimes surprising, but it could be done. I'm not saying that this is a good approach, I'm saying that the vagueness of principle encompasses it.

Yours,
    Thomas.






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