equal
deleted
inserted
replaced
273 |
273 |
274 fun CONJ_WRAP_GEN' conj_tac gen_tac xs = |
274 fun CONJ_WRAP_GEN' conj_tac gen_tac xs = |
275 let val (butlast, last) = split_last xs; |
275 let val (butlast, last) = split_last xs; |
276 in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end; |
276 in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end; |
277 |
277 |
278 fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac; |
278 fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (resolve0_tac [conjI] 1) gen_tac; |
279 fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac; |
279 fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (resolve0_tac [conjI]) gen_tac; |
280 |
280 |
281 fun rtac ctxt thm = resolve_tac ctxt [thm]; |
281 fun rtac ctxt thm = resolve_tac ctxt [thm]; |
282 fun etac ctxt thm = eresolve_tac ctxt [thm]; |
282 fun etac ctxt thm = eresolve_tac ctxt [thm]; |
283 fun dtac ctxt thm = dresolve_tac ctxt [thm]; |
283 fun dtac ctxt thm = dresolve_tac ctxt [thm]; |
284 fun ftac ctxt thm = forward_tac ctxt [thm]; |
284 fun ftac ctxt thm = forward_tac ctxt [thm]; |