# HG changeset patch
# User paulson
# Date 967113582 -7200
# Node ID 87b460d72e80f9c0d6d695ec3565c2eab9479acc
# Parent  6d123a7e30bd15982b938cccc6099955935f3f28
xsymbols for {| and |}

diff -r 6d123a7e30bd -r 87b460d72e80 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Thu Aug 24 12:39:24 2000 +0200
+++ b/src/HOL/Auth/Message.thy	Thu Aug 24 12:39:42 2000 +0200
@@ -42,6 +42,9 @@
 syntax
   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
 
+syntax (xsymbols)
+  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\\<lbrace>_,/ _\\<rbrace>)")
+
 translations
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
   "{|x, y|}"      == "MPair x y"