diff -r ff3a86a00ea5 -r 5cacc383157a src/ZF/Integ/EquivClass.thy
--- a/src/ZF/Integ/EquivClass.thy	Thu Jul 13 23:26:08 2000 +0200
+++ b/src/ZF/Integ/EquivClass.thy	Fri Jul 14 13:39:03 2000 +0200
@@ -7,17 +7,17 @@
 *)
 
 EquivClass = Rel + Perm + 
-consts
-    "'/"        ::      [i,i]=>i  (infixl 90)  (*set of equiv classes*)
-    congruent   ::      [i,i=>i]=>o
-    congruent2  ::      [i,[i,i]=>i]=>o
+
+constdefs
+
+  quotient    :: [i,i]=>i    (infixl "'/'/" 90)  (*set of equiv classes*)
+      "A//r == {r``{x} . x:A}"
 
-defs
-    quotient_def  "A/r == {r``{x} . x:A}"
-    congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
+  congruent   :: [i,i=>i]=>o
+      "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
 
-    congruent2_def
-       "congruent2(r,b) == ALL y1 z1 y2 z2. 
+  congruent2  :: [i,[i,i]=>i]=>o
+      "congruent2(r,b) == ALL y1 z1 y2 z2. 
            <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
 
 end