Nominal/Nominal2.thy
changeset 2950 0911cb7bf696
parent 2943 09834ba7ce59
child 2957 01ff621599bc
equal deleted inserted replaced
2949:adf22ee09738 2950:0911cb7bf696
   677   fun tuple1 ((x, y, z), u) = (x, y, z, u)
   677   fun tuple1 ((x, y, z), u) = (x, y, z, u)
   678   fun tuple2 (((x, y), z), u) = (x, y, u, z)
   678   fun tuple2 (((x, y), z), u) = (x, y, u, z)
   679   fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
   679   fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
   680 in
   680 in
   681 
   681 
   682 val _ = Keyword.keyword "bind"
   682 val _ = Keyword.keyword "binds"
   683 
   683 
   684 val opt_name = Scan.option (P.binding --| Args.colon)
   684 val opt_name = Scan.option (P.binding --| Args.colon)
   685 
   685 
   686 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
   686 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
   687 
   687 
   688 val bind_mode = P.$$$ "bind" |--
   688 val bind_mode = P.$$$ "binds" |--
   689   S.optional (Args.parens 
   689   S.optional (Args.parens 
   690     (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst
   690     (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst
   691 
   691 
   692 val bind_clauses = 
   692 val bind_clauses = 
   693   P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)
   693   P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)