equal
deleted
inserted
replaced
310 |
310 |
311 |
311 |
312 (* outer syntax *) |
312 (* outer syntax *) |
313 |
313 |
314 val _ = |
314 val _ = |
315 Outer_Syntax.local_theory @{command_spec "primrec"} |
315 Outer_Syntax.local_theory @{command_spec "old_primrec"} |
316 "define primitive recursive functions on datatypes" |
316 "define primitive recursive functions on datatypes" |
317 (Parse.fixes -- Parse_Spec.where_alt_specs |
317 (Parse.fixes -- Parse_Spec.where_alt_specs |
318 >> (fn (fixes, specs) => add_primrec_cmd fixes specs #> snd)); |
318 >> (fn (fixes, specs) => add_primrec_cmd fixes specs #> snd)); |
319 |
319 |
320 end; |
320 end; |