equal
deleted
inserted
replaced
5 |
5 |
6 structure NominalInduct: |
6 structure NominalInduct: |
7 sig |
7 sig |
8 val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> |
8 val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> |
9 (string * typ) list -> (string * typ) list list -> thm list -> |
9 (string * typ) list -> (string * typ) list list -> thm list -> |
10 thm list -> int -> Rule_Cases.cases_tactic |
10 thm list -> int -> cases_tactic |
11 val nominal_induct_method: (Proof.context -> Proof.method) context_parser |
11 val nominal_induct_method: (Proof.context -> Proof.method) context_parser |
12 end = |
12 end = |
13 struct |
13 struct |
14 |
14 |
15 (* proper tuples -- nested left *) |
15 (* proper tuples -- nested left *) |