equal
deleted
inserted
replaced
43 (take n cases ~~ take n hnamess); |
43 (take n cases ~~ take n hnamess); |
44 in ((cases', consumes), th) end; |
44 in ((cases', consumes), th) end; |
45 |
45 |
46 val induction_tac = Induct.gen_induct_tac (K name_hyps); |
46 val induction_tac = Induct.gen_induct_tac (K name_hyps); |
47 |
47 |
48 val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac); |
48 val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac); |
49 |
49 |
50 end |
50 end |