equal
deleted
inserted
replaced
68 fun case_product_tac prems struc thm1 thm2 = |
68 fun case_product_tac prems struc thm1 thm2 = |
69 let |
69 let |
70 val (p_cons1 :: p_cons2 :: premss) = unflat struc prems |
70 val (p_cons1 :: p_cons2 :: premss) = unflat struc prems |
71 val thm2' = thm2 OF p_cons2 |
71 val thm2' = thm2 OF p_cons2 |
72 in |
72 in |
73 Tactic.rtac (thm1 OF p_cons1) |
73 rtac (thm1 OF p_cons1) |
74 THEN' EVERY' (map (fn p => |
74 THEN' EVERY' (map (fn p => |
75 Tactic.rtac thm2' |
75 rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss) |
76 THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss) |
|
77 end |
76 end |
78 |
77 |
79 fun combine ctxt thm1 thm2 = |
78 fun combine ctxt thm1 thm2 = |
80 let |
79 let |
81 val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt |
80 val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt |