*To*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Subject*: Re: [isabelle] theory_of_thm @{thm xxx}*From*: Makarius <makarius at sketis.net>*Date*: Wed, 22 Aug 2012 13:19:09 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50346EA9.5020806@nicta.com.au>*References*: <1345567640.6244.6.camel@lapbroy33> <50346EA9.5020806@nicta.com.au>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 22 Aug 2012, Thomas Sewell wrote:

In principle, having @{thm meta_mp} live only in @{theory Pure} would makeperfect sense.In practice, this would create a problem if you tried, say: theory Scratch imports A B begin ML_val {* Thm.transitive @{thm A.eq1} @{thm B.eq2} *}How does Thm.transitive figure out an appropriate context for a rule derivedfrom A.eq1 and B.eq2?To avoid this problem, A.eq1 and B.eq2 are "pulled" up into theoryScratch when they are fetched, thus allowing derivation operations toproceed without doing any interesting work.There are other ways in ML to fetch these theorems in their originalcontext, at which point if you attempt resolution or similar you willsee the error "Attempt to perform non-trivial merge of theories" fromPure/context.ML.

Makarius

**Follow-Ups**:**Re: [isabelle] theory_of_thm @{thm xxx}***From:*Thomas Sewell

**References**:**[isabelle] theory_of_thm @{thm xxx}***From:*Peter Lammich

**Re: [isabelle] theory_of_thm @{thm xxx}***From:*Thomas Sewell

- Previous by Date: Re: [isabelle] theory_of_thm @{thm xxx}
- Next by Date: Re: [isabelle] theory_of_thm @{thm xxx}
- Previous by Thread: Re: [isabelle] theory_of_thm @{thm xxx}
- Next by Thread: Re: [isabelle] theory_of_thm @{thm xxx}
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list