equal
deleted
inserted
replaced
1 signature INDUCTION = |
1 signature INDUCTION = |
2 sig |
2 sig |
3 val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> |
3 val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> |
4 (string * typ) list list -> term option list -> thm list option -> |
4 (string * typ) list list -> term option list -> thm list option -> |
5 thm list -> int -> cases_tactic |
5 thm list -> int -> cases_tactic |
6 val setup: theory -> theory |
|
7 end |
6 end |
8 |
7 |
9 structure Induction: INDUCTION = |
8 structure Induction: INDUCTION = |
10 struct |
9 struct |
11 |
10 |
35 (take n cases ~~ take n hnamess) |
34 (take n cases ~~ take n hnamess) |
36 in ((cases',consumes),th) end |
35 in ((cases',consumes),th) end |
37 |
36 |
38 val induction_tac = Induct.gen_induct_tac (K name_hyps) |
37 val induction_tac = Induct.gen_induct_tac (K name_hyps) |
39 |
38 |
40 val setup = Induct.gen_induct_setup @{binding induction} induction_tac |
39 val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac) |
41 |
40 |
42 end |
41 end |
43 |
42 |