equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature IND_CASES = |
8 signature IND_CASES = |
9 sig |
9 sig |
10 val declare: string -> (simpset -> cterm -> thm) -> theory -> theory |
10 val declare: string -> (simpset -> cterm -> thm) -> theory -> theory |
11 val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory |
11 val inductive_cases: ((Name.binding * Attrib.src list) * string list) list -> theory -> theory |
12 val setup: theory -> theory |
12 val setup: theory -> theory |
13 end; |
13 end; |
14 |
14 |
15 structure IndCases: IND_CASES = |
15 structure IndCases: IND_CASES = |
16 struct |
16 struct |