equal
deleted
inserted
replaced
88 val transfer_cterm: theory -> cterm -> cterm |
88 val transfer_cterm: theory -> cterm -> cterm |
89 val transfer: theory -> thm -> thm |
89 val transfer: theory -> thm -> thm |
90 val transfer': Proof.context -> thm -> thm |
90 val transfer': Proof.context -> thm -> thm |
91 val transfer'': Context.generic -> thm -> thm |
91 val transfer'': Context.generic -> thm -> thm |
92 val join_transfer: theory -> thm -> thm |
92 val join_transfer: theory -> thm -> thm |
|
93 val join_transfer_context: Proof.context * thm -> Proof.context * thm |
93 val renamed_prop: term -> thm -> thm |
94 val renamed_prop: term -> thm -> thm |
94 val weaken: cterm -> thm -> thm |
95 val weaken: cterm -> thm -> thm |
95 val weaken_sorts: sort list -> cterm -> cterm |
96 val weaken_sorts: sort list -> cterm -> cterm |
96 val extra_shyps: thm -> sort list |
97 val extra_shyps: thm -> sort list |
97 val proof_bodies_of: thm list -> proof_body list |
98 val proof_bodies_of: thm list -> proof_body list |
532 val transfer'' = transfer o Context.theory_of; |
533 val transfer'' = transfer o Context.theory_of; |
533 |
534 |
534 fun join_transfer thy th = |
535 fun join_transfer thy th = |
535 if Context.subthy_id (Context.theory_id thy, theory_id th) then th |
536 if Context.subthy_id (Context.theory_id thy, theory_id th) then th |
536 else transfer thy th; |
537 else transfer thy th; |
|
538 |
|
539 fun join_transfer_context (ctxt, th) = |
|
540 if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then |
|
541 (Context.raw_transfer (theory_of_thm th) ctxt, th) |
|
542 else (ctxt, transfer' ctxt th); |
537 |
543 |
538 |
544 |
539 (* matching *) |
545 (* matching *) |
540 |
546 |
541 local |
547 local |