src/HOL/Auth/Message.thy
changeset 35109 0015a0a99ae9
parent 35054 a5db9779b026
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Auth/Message.thy	Thu Feb 11 21:31:50 2010 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Feb 11 21:33:25 2010 +0100
     1.3 @@ -51,10 +51,10 @@
     1.4  
     1.5  text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
     1.6  syntax
     1.7 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     1.8 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     1.9  
    1.10  syntax (xsymbols)
    1.11 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    1.12 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    1.13  
    1.14  translations
    1.15    "{|x, y, z|}"   == "{|x, {|y, z|}|}"