src/HOL/Auth/Message.thy
changeset 9686 87b460d72e80
parent 7057 b9ddbb925939
child 10833 c0844a30ea4e
     1.1 --- a/src/HOL/Auth/Message.thy	Thu Aug 24 12:39:24 2000 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Aug 24 12:39:42 2000 +0200
     1.3 @@ -42,6 +42,9 @@
     1.4  syntax
     1.5    "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     1.6  
     1.7 +syntax (xsymbols)
     1.8 +  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\\<lbrace>_,/ _\\<rbrace>)")
     1.9 +
    1.10  translations
    1.11    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    1.12    "{|x, y|}"      == "MPair x y"