129 calc : calc list, (*for Calculate in scr, set by prep_rls *) |
129 calc : calc list, (*for Calculate in scr, set by prep_rls *) |
130 scr : scr}; (*Rfuns {...} (how to restrict type ???)*) |
130 scr : scr}; (*Rfuns {...} (how to restrict type ???)*) |
131 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently |
131 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently |
132 from rls, and then contain both Script _AND_ Rfuns !!!*) |
132 from rls, and then contain both Script _AND_ Rfuns !!!*) |
133 |
133 |
|
134 fun thy2ctxt thy' = ProofContext.init_global (theory thy'); (*FIXXXME thy-ctxt*) |
134 |
135 |
135 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*) |
136 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*) |
136 val ctxt_HOL = ProofContext.init_global (theory "Complex_Main"); |
137 (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*) |
137 val HOL = ProofContext.theory_of ctxt_HOL; |
138 val ctxt_HOL = thy2ctxt "Complex_Main"; |
138 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*) |
139 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*) |
139 fun ctxt_Isac _ = ProofContext.init_global (theory "Isac"); |
140 fun ctxt_Isac _ = thy2ctxt "Isac"; |
140 fun Isac _ = ProofContext.theory_of (ctxt_Isac""); |
141 fun Isac _ = ProofContext.theory_of (ctxt_Isac""); |
141 |
142 |
142 val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" ); |
143 val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" ); |
143 fun id_of_thm (Thm (id, _)) = id |
144 fun id_of_thm (Thm (id, _)) = id |
144 | id_of_thm _ = raise error "id_of_thm"; |
145 | id_of_thm _ = raise error "id_of_thm"; |