| changeset 3135 | 92b9b8d2888d |
| parent 3134 | 301b74fcd614 |
| child 3157 | de89c95c5377 |
| 3134:301b74fcd614 | 3135:92b9b8d2888d |
|---|---|
708 fun triple2 ((x, y), z) = (y, x, z) |
708 fun triple2 ((x, y), z) = (y, x, z) |
709 fun tuple2 (((x, y), z), u) = (x, y, u, z) |
709 fun tuple2 (((x, y), z), u) = (x, y, u, z) |
710 fun tuple3 ((x, y), (z, u)) = (x, y, z, u) |
710 fun tuple3 ((x, y), (z, u)) = (x, y, z, u) |
711 in |
711 in |
712 |
712 |
713 val _ = Keyword.keyword "binds" |
|
714 |
|
715 val opt_name = Scan.option (P.binding --| Args.colon) |
713 val opt_name = Scan.option (P.binding --| Args.colon) |
716 |
714 |
717 val anno_typ = S.option (P.name --| @{keyword "::"}) -- P.typ |
715 val anno_typ = S.option (P.name --| @{keyword "::"}) -- P.typ |
718 |
716 |
719 val bind_mode = @{keyword "binds"} |-- |
717 val bind_mode = @{keyword "binds"} |-- |
740 opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3 |
738 opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3 |
741 |
739 |
742 end |
740 end |
743 |
741 |
744 (* Command Keyword *) |
742 (* Command Keyword *) |
745 val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl |
743 val _ = Outer_Syntax.local_theory ("nominal_datatype", Keyword.thy_decl) |
746 (main_parser >> nominal_datatype2_cmd) |
744 "declaration of nominal datatypes" |
747 *} |
745 (main_parser >> nominal_datatype2_cmd) |
748 |
746 *} |
749 |
747 |
750 end |
748 |
751 |
749 end |
752 |
750 |
753 |
751 |
752 |