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*)