equal
deleted
inserted
replaced
746 opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3 |
746 opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3 |
747 |
747 |
748 end |
748 end |
749 |
749 |
750 (* Command Keyword *) |
750 (* Command Keyword *) |
751 val _ = Outer_Syntax.local_theory ("nominal_datatype", Keyword.thy_decl) |
751 val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} |
752 "declaration of nominal datatypes" |
752 "declaration of nominal datatypes" |
753 (main_parser >> nominal_datatype2_cmd) |
753 (main_parser >> nominal_datatype2_cmd) |
754 *} |
754 *} |
755 |
755 |
756 |
756 |