src/ZF/EquivClass.thy

--- a/src/ZF/EquivClass.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/EquivClass.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -17,7 +17,7 @@
     congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
 
     congruent2_def
-       "congruent2(r,b) == ALL y1 z1 y2 z2. \
-\           <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
+       "congruent2(r,b) == ALL y1 z1 y2 z2. 
+           <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
 
 end