equal
deleted
inserted
replaced
317 lemmas adm_lemmas = |
317 lemmas adm_lemmas = |
318 adm_not_free adm_eq adm_less adm_not_less |
318 adm_not_free adm_eq adm_less adm_not_less |
319 adm_not_eq_tr adm_conj adm_disj adm_imp adm_all |
319 adm_not_eq_tr adm_conj adm_disj adm_imp adm_all |
320 |
320 |
321 method_setup induct = \<open> |
321 method_setup induct = \<open> |
322 Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt => |
322 Scan.lift Args.embedded_inner_syntax >> (fn v => fn ctxt => |
323 SIMPLE_METHOD' (fn i => |
323 SIMPLE_METHOD' (fn i => |
324 Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] [] @{thm induct} i THEN |
324 Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] [] @{thm induct} i THEN |
325 REPEAT (resolve_tac ctxt @{thms adm_lemmas} i))) |
325 REPEAT (resolve_tac ctxt @{thms adm_lemmas} i))) |
326 \<close> |
326 \<close> |
327 |
327 |