equal
deleted
inserted
replaced
589 Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] -- |
589 Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] -- |
590 Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) [] |
590 Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) [] |
591 >> (Toplevel.theory o mk_ind); |
591 >> (Toplevel.theory o mk_ind); |
592 |
592 |
593 val _ = |
593 val _ = |
594 Outer_Syntax.command (co_prefix ^ "inductive") |
594 Outer_Syntax.command |
595 ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl; |
595 (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"}) |
|
596 ("define " ^ co_prefix ^ "inductive sets") ind_decl; |
596 |
597 |
597 end; |
598 end; |
598 |
599 |