equal
deleted
inserted
replaced
44 val cases' = |
44 val cases' = |
45 map (fn (((cn, _), concls), hns) => ((cn, hns), concls)) |
45 map (fn (((cn, _), concls), hns) => ((cn, hns), concls)) |
46 (take n cases ~~ take n hnamess); |
46 (take n cases ~~ take n hnamess); |
47 in ((cases', consumes), th) end); |
47 in ((cases', consumes), th) end); |
48 |
48 |
49 fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 = |
49 fun induction_tac ctxt simp def_insts arbitrary taking opt_rule facts i = |
50 NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7); |
50 induction_context_tactic simp def_insts arbitrary taking opt_rule facts i |
|
51 |> NO_CONTEXT_TACTIC ctxt; |
51 |
52 |
52 val _ = |
53 val _ = |
53 Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic); |
54 Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic); |
54 |
55 |
55 end |
56 end |