equal
deleted
inserted
replaced
1887 Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes" |
1887 Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes" |
1888 (parse_co_datatype_cmd Least_FP construct_lfp); |
1888 (parse_co_datatype_cmd Least_FP construct_lfp); |
1889 |
1889 |
1890 val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"} |
1890 val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"} |
1891 "define primitive recursive functions" |
1891 "define primitive recursive functions" |
1892 (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_primrec_cmd); |
1892 (Parse.fixes -- Parse_Spec.where_alt_specs >> (snd oo uncurry add_primrec_cmd)); |
1893 |
1893 |
1894 end; |
1894 end; |