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