# HG changeset patch
# User nipkow
# Date 808754062 -7200
# Node ID 454eb424c2230d17033e16773faf81cbd045d361
# Parent  91d2c1bb580377cce9fc1ff68ba9b26d11158393
changed "o" to (infixl 55)

diff -r 91d2c1bb5803 -r 454eb424c223 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Aug 18 15:20:02 1995 +0200
+++ b/src/HOL/HOL.thy	Fri Aug 18 15:54:22 1995 +0200
@@ -51,7 +51,7 @@
 
   (* Infixes *)
 
-  o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixr 50)
+  o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl 55)
   "="           :: "['a, 'a] => bool"                 (infixl 50)
   "&"           :: "[bool, bool] => bool"             (infixr 35)
   "|"           :: "[bool, bool] => bool"             (infixr 30)