equal
deleted
inserted
replaced
186 |
186 |
187 (* outer syntax *) |
187 (* outer syntax *) |
188 |
188 |
189 local structure P = OuterParse and K = OuterKeyword in |
189 local structure P = OuterParse and K = OuterKeyword in |
190 |
190 |
191 val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"]; |
191 val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"]; |
192 |
192 |
193 val rep_datatype_decl = |
193 val rep_datatype_decl = |
194 (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) -- |
194 (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) -- |
195 (P.$$$ "induction" |-- P.!!! SpecParse.xthm) -- |
195 (P.$$$ "induction" |-- P.!!! SpecParse.xthm) -- |
196 (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) -- |
196 (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) -- |