# HG changeset patch
# User wenzelm
# Date 963773315 -7200
# Node ID 416b2ecd97a173caffa66c3a4745e0cfbb18107c
# Parent  5d53e3f35152f500d910c61b91bdb237afe43905
syntax (symbols) "op o" moved from HOL to Fun;

diff -r 5d53e3f35152 -r 416b2ecd97a1 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Jul 16 20:47:45 2000 +0200
+++ b/src/HOL/Fun.thy	Sun Jul 16 20:48:35 2000 +0200
@@ -49,6 +49,9 @@
   inj_on :: ['a => 'b, 'a set] => bool
     "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
 
+syntax (symbols)
+  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
+
 syntax
   inj   :: ('a => 'b) => bool                   (*injective*)
 
diff -r 5d53e3f35152 -r 416b2ecd97a1 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Jul 16 20:47:45 2000 +0200
+++ b/src/HOL/HOL.thy	Sun Jul 16 20:48:35 2000 +0200
@@ -113,7 +113,6 @@
   "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
   "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
   "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
-  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
   "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
   "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)