184 "datatype case_tac emulation (dynamic instantiation!)"; |
184 "datatype case_tac emulation (dynamic instantiation!)"; |
185 |
185 |
186 |
186 |
187 (* outer syntax *) |
187 (* outer syntax *) |
188 |
188 |
189 local structure P = OuterParse and K = OuterKeyword in |
189 val _ = List.app Keyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"]; |
190 |
|
191 val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"]; |
|
192 |
190 |
193 val rep_datatype_decl = |
191 val rep_datatype_decl = |
194 (P.$$$ "elimination" |-- P.!!! Parse_Spec.xthm) -- |
192 (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) -- |
195 (P.$$$ "induction" |-- P.!!! Parse_Spec.xthm) -- |
193 (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) -- |
196 (P.$$$ "case_eqns" |-- P.!!! Parse_Spec.xthms1) -- |
194 (Parse.$$$ "case_eqns" |-- Parse.!!! Parse_Spec.xthms1) -- |
197 Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! Parse_Spec.xthms1) [] |
195 Scan.optional (Parse.$$$ "recursor_eqns" |-- Parse.!!! Parse_Spec.xthms1) [] |
198 >> (fn (((x, y), z), w) => rep_datatype x y z w); |
196 >> (fn (((x, y), z), w) => rep_datatype x y z w); |
199 |
197 |
200 val _ = |
198 val _ = |
201 OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl |
199 Outer_Syntax.command "rep_datatype" "represent existing set inductively" Keyword.thy_decl |
202 (rep_datatype_decl >> Toplevel.theory); |
200 (rep_datatype_decl >> Toplevel.theory); |
203 |
201 |
204 end; |
202 end; |
205 |
|
206 end; |
|
207 |
|
208 |
203 |
209 val exhaust_tac = DatatypeTactics.exhaust_tac; |
204 val exhaust_tac = DatatypeTactics.exhaust_tac; |
210 val induct_tac = DatatypeTactics.induct_tac; |
205 val induct_tac = DatatypeTactics.induct_tac; |