Fixed pretty-printing of {|...|}
authorpaulson
Tue, 03 Sep 1996 19:07:23 +0200
changeset 1947 f19a801a2bca
parent 1946 b59a3d686436
child 1948 78e5bfcbc1e9
Fixed pretty-printing of {|...|}
src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Tue Sep 03 19:07:00 1996 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Sep 03 19:07:23 1996 +0200
@@ -55,7 +55,7 @@
 
 (*Allows messages of the form {|A,B,NA|}, etc...*)
 syntax
-  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
+  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(2{|_,/ _|})")
 
 translations
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"