equal
deleted
inserted
replaced
644 (** outer syntax **) |
644 (** outer syntax **) |
645 |
645 |
646 local open OuterParse in |
646 local open OuterParse in |
647 |
647 |
648 fun mk_ind coind (((sets, intrs), monos), con_defs) = |
648 fun mk_ind coind (((sets, intrs), monos), con_defs) = |
649 #1 o add_inductive true coind sets (map (fn ((x, y), z) => ((x, z), y)) intrs) monos con_defs; |
649 #1 o add_inductive true coind sets (map triple_swap intrs) monos con_defs; |
650 |
650 |
651 fun ind_decl coind = |
651 fun ind_decl coind = |
652 Scan.repeat1 term -- |
652 Scan.repeat1 term -- |
653 ($$$ "intrs" |-- !!! (Scan.repeat1 (opt_thm_name ":" -- term))) -- |
653 ($$$ "intrs" |-- !!! (Scan.repeat1 (opt_thm_name ":" -- term))) -- |
654 Scan.optional ($$$ "monos" |-- !!! xthms1) [] -- |
654 Scan.optional ($$$ "monos" |-- !!! xthms1) [] -- |