197 |
197 |
198 |
198 |
199 fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt) |
199 fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt) |
200 |
200 |
201 val by_pat_completeness_simp = |
201 val by_pat_completeness_simp = |
202 Proof.global_terminal_proof |
202 Proof.future_terminal_proof |
203 (Method.Basic (pat_completeness, Position.none), |
203 (Method.Basic (pat_completeness, Position.none), |
204 SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) |
204 SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) |
205 |
205 |
206 fun termination_by method = |
206 fun termination_by method = |
207 FundefPackage.setup_termination_proof NONE |
207 FundefPackage.setup_termination_proof NONE |
208 #> Proof.global_terminal_proof |
208 #> Proof.future_terminal_proof |
209 (Method.Basic (method, Position.none), NONE) |
209 (Method.Basic (method, Position.none), NONE) |
210 |
210 |
211 fun mk_catchall fixes arities = |
211 fun mk_catchall fixes arities = |
212 let |
212 let |
213 fun mk_eqn ((fname, fT), _) = |
213 fun mk_eqn ((fname, fT), _) = |