206 |
206 |
207 fun pat_completeness ctxt = SIMPLE_METHOD' (pat_completeness_tac ctxt) |
207 fun pat_completeness ctxt = SIMPLE_METHOD' (pat_completeness_tac ctxt) |
208 |
208 |
209 val by_pat_completeness_auto = |
209 val by_pat_completeness_auto = |
210 Proof.global_future_terminal_proof |
210 Proof.global_future_terminal_proof |
211 (Method.Basic (pat_completeness, Position.none), |
211 (Method.Basic pat_completeness, |
212 SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) |
212 SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) |
213 |
213 |
214 fun termination_by method int = |
214 fun termination_by method int = |
215 Fundef.termination_proof NONE |
215 Fundef.termination_proof NONE |
216 #> Proof.global_future_terminal_proof |
216 #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int |
217 (Method.Basic (method, Position.none), NONE) int |
|
218 |
217 |
219 fun mk_catchall fixes arity_of = |
218 fun mk_catchall fixes arity_of = |
220 let |
219 let |
221 fun mk_eqn ((fname, fT), _) = |
220 fun mk_eqn ((fname, fT), _) = |
222 let |
221 let |