xsymbols for {| and |}
authorpaulson
Thu Aug 24 12:39:42 2000 +0200 (2000-08-24)
changeset 968687b460d72e80
parent 9685 6d123a7e30bd
child 9687 772ac061bd76
xsymbols for {| and |}
src/HOL/Auth/Message.thy
     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"