equal
deleted
inserted
replaced
221 case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl) |
221 case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl) |
222 (mk_dom xs) Net.empty 0 0 of |
222 (mk_dom xs) Net.empty 0 0 of |
223 NONE => no_tac |
223 NONE => no_tac |
224 | SOME prf => |
224 | SOME prf => |
225 rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1 |
225 rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1 |
226 end) ctxt 1) ctxt; |
226 end) context 1) ctxt; |
227 |
227 |
228 fun coherent_meth rules ctxt = |
228 fun coherent_meth rules ctxt = |
229 Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1); |
229 Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1); |
230 |
230 |
231 val setup = Method.add_method |
231 val setup = Method.add_method |