equal
deleted
inserted
replaced
39 |
39 |
40 |
40 |
41 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*) |
41 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*) |
42 syntax |
42 syntax |
43 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
43 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
|
44 |
|
45 syntax (xsymbols) |
|
46 "@MTuple" :: "['a, args] => 'a * 'b" ("(2\\<lbrace>_,/ _\\<rbrace>)") |
44 |
47 |
45 translations |
48 translations |
46 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
49 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
47 "{|x, y|}" == "MPair x y" |
50 "{|x, y|}" == "MPair x y" |
48 |
51 |