equal
deleted
inserted
replaced
4 The nominal induct proof method. |
4 The nominal induct proof method. |
5 *) |
5 *) |
6 |
6 |
7 structure NominalInduct: |
7 structure NominalInduct: |
8 sig |
8 sig |
9 val nominal_induct_tac: Proof.context -> (Binding.T option * term) option list list -> |
9 val nominal_induct_tac: Proof.context -> (binding option * term) option list list -> |
10 (string * typ) list -> (string * typ) list list -> thm list -> |
10 (string * typ) list -> (string * typ) list list -> thm list -> |
11 thm list -> int -> RuleCases.cases_tactic |
11 thm list -> int -> RuleCases.cases_tactic |
12 val nominal_induct_method: Method.src -> Proof.context -> Method.method |
12 val nominal_induct_method: Method.src -> Proof.context -> Method.method |
13 end = |
13 end = |
14 struct |
14 struct |