equal
deleted
inserted
replaced
577 |
577 |
578 |
578 |
579 (* outer syntax *) |
579 (* outer syntax *) |
580 |
580 |
581 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) = |
581 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) = |
582 #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims); |
582 #1 o add_inductive doms (map (fn ((x, y), z) => ((x, z), y)) intrs) |
|
583 (monos, con_defs, type_intrs, type_elims); |
583 |
584 |
584 val ind_decl = |
585 val ind_decl = |
585 (@{keyword "domains"} |-- Parse.!!! (Parse.enum1 "+" Parse.term -- |
586 (@{keyword "domains"} |-- Parse.!!! (Parse.enum1 "+" Parse.term -- |
586 ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) -- |
587 ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) -- |
587 (@{keyword "intros"} |-- |
588 (@{keyword "intros"} |-- |