equal
deleted
inserted
replaced
80 *} |
80 *} |
81 |
81 |
82 (*<*) |
82 (*<*) |
83 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*} |
83 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*} |
84 syntax |
84 syntax |
85 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
85 "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
86 |
86 |
87 syntax (xsymbols) |
87 syntax (xsymbols) |
88 "@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
88 "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
89 |
89 |
90 translations |
90 translations |
91 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
91 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
92 "{|x, y|}" == "MPair x y" |
92 "{|x, y|}" == "CONST MPair x y" |
93 |
93 |
94 |
94 |
95 constdefs |
95 constdefs |
96 keysFor :: "msg set => key set" |
96 keysFor :: "msg set => key set" |
97 --{*Keys useful to decrypt elements of a message set*} |
97 --{*Keys useful to decrypt elements of a message set*} |