equal
deleted
inserted
replaced
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 x1 x2 x3 x4 x5 x6 x7 = |
50 Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7); |
50 NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7); |
51 |
51 |
52 val _ = |
52 val _ = |
53 Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic); |
53 Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic); |
54 |
54 |
55 end |
55 end |