src/ZF/EquivClass.thy

--- a/src/ZF/EquivClass.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/EquivClass.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
 
 EquivClass = Rel + Perm + 
 consts
-    "'/"        ::      "[i,i]=>i"  (infixl 90)  (*set of equiv classes*)
-    congruent	::	"[i,i=>i]=>o"
-    congruent2  ::      "[i,[i,i]=>i]=>o"
+    "'/"        ::      [i,i]=>i  (infixl 90)  (*set of equiv classes*)
+    congruent	::	[i,i=>i]=>o
+    congruent2  ::      [i,[i,i]=>i]=>o
 
 defs
     quotient_def  "A/r == {r``{x} . x:A}"