equal
deleted
inserted
replaced
749 #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs; |
749 #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs; |
750 |
750 |
751 fun ind_decl coind = |
751 fun ind_decl coind = |
752 (Scan.repeat1 P.term --| P.marg_comment) -- |
752 (Scan.repeat1 P.term --| P.marg_comment) -- |
753 (P.$$$ "intrs" |-- |
753 (P.$$$ "intrs" |-- |
754 P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment))) -- |
754 P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) -- |
755 Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- |
755 Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- |
756 Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] |
756 Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] |
757 >> (Toplevel.theory o mk_ind coind); |
757 >> (Toplevel.theory o mk_ind coind); |
758 |
758 |
759 val inductiveP = |
759 val inductiveP = |