# HG changeset patch
# User nipkow
# Date 765014423 -7200
# Node ID ee7413a7a44af378b6ff1b5d5b46871bfa321a65
# Parent  94436622324d5ba94c2af982a9f6f415f6d4fbe8
@ now associates to the right, just like #, in order to avoid loss of
parentheses due to pretty printer.

diff -r 94436622324d -r ee7413a7a44a List.thy
--- a/List.thy	Sun Mar 27 16:43:06 1994 +0200
+++ b/List.thy	Wed Mar 30 10:00:23 1994 +0200
@@ -40,7 +40,7 @@
   mem		:: "['a, 'a list] => bool"			(infixl 55)
   list_all      :: "('a => bool) => ('a list => bool)"
   map           :: "('a=>'b) => ('a list => 'b list)"
-  "@"		:: "['a list, 'a list] => 'a list"		(infixl 65)
+  "@"		:: "['a list, 'a list] => 'a list"		(infixr 65)
   list_case     :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
   filter	:: "['a => bool, 'a list] => 'a list"