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