equal
deleted
inserted
replaced
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: ((bstring * Attrib.src list) * string list) list -> theory -> theory |
12 val setup: (theory -> theory) list |
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 |
17 |
17 |
70 |
70 |
71 |
71 |
72 (* package setup *) |
72 (* package setup *) |
73 |
73 |
74 val setup = |
74 val setup = |
75 [IndCasesData.init, |
75 (IndCasesData.init #> |
76 Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, |
76 Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, |
77 "dynamic case analysis on sets")]]; |
77 "dynamic case analysis on sets")]); |
78 |
78 |
79 |
79 |
80 (* outer syntax *) |
80 (* outer syntax *) |
81 |
81 |
82 local structure P = OuterParse and K = OuterKeyword in |
82 local structure P = OuterParse and K = OuterKeyword in |