equal
deleted
inserted
replaced
1028 (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype)); |
1028 (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype)); |
1029 |
1029 |
1030 |
1030 |
1031 val rep_datatype_decl = |
1031 val rep_datatype_decl = |
1032 Scan.option (Scan.repeat1 P.name) -- |
1032 Scan.option (Scan.repeat1 P.name) -- |
1033 Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [[]] -- |
1033 Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] -- |
1034 Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] -- |
1034 Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] -- |
1035 (P.$$$ "induction" |-- P.!!! P.xthm); |
1035 (P.$$$ "induction" |-- P.!!! SpecParse.xthm); |
1036 |
1036 |
1037 fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind; |
1037 fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind; |
1038 |
1038 |
1039 val rep_datatypeP = |
1039 val rep_datatypeP = |
1040 OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl |
1040 OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl |