equal
deleted
inserted
replaced
201 args) thy; |
201 args) thy; |
202 |
202 |
203 |
203 |
204 (* outer syntax *) |
204 (* outer syntax *) |
205 |
205 |
206 local structure P = OuterParse and K = OuterKeyword in |
206 structure P = OuterParse and K = OuterKeyword; |
207 |
207 |
208 val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop); |
208 val _ = |
209 |
|
210 val primrecP = |
|
211 OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl |
209 OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl |
212 (primrec_decl >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap)))); |
210 (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) |
213 |
211 >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap)))); |
214 val _ = OuterSyntax.add_parsers [primrecP]; |
|
215 |
212 |
216 end; |
213 end; |
217 |
214 |
218 end; |
|
219 |
|
220 |
|