equal
deleted
inserted
replaced
5 name "IH". |
5 name "IH". |
6 *) |
6 *) |
7 |
7 |
8 signature INDUCTION = |
8 signature INDUCTION = |
9 sig |
9 sig |
10 val induction_tac: Proof.context -> bool -> |
10 val induction_tac: bool -> (binding option * (term * bool)) option list list -> |
11 (binding option * (term * bool)) option list list -> |
|
12 (string * typ) list list -> term option list -> thm list option -> |
11 (string * typ) list list -> term option list -> thm list option -> |
13 thm list -> int -> cases_tactic |
12 thm list -> int -> context_tactic |
14 end |
13 end |
15 |
14 |
16 structure Induction: INDUCTION = |
15 structure Induction: INDUCTION = |
17 struct |
16 struct |
18 |
17 |