src/ZF/Rel.thy
changeset 1155 928a16e02f9f
parent 753 ec86863e87c8
child 1401 0c439768f45c
--- a/src/ZF/Rel.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Rel.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -25,8 +25,8 @@
 
   trans_def    "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
 
-  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. 	\
-\                          <x,y>: r --> <y,z>: r --> <x,z>: r"
+  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. 	
+                          <x,y>: r --> <y,z>: r --> <x,z>: r"
 
   equiv_def    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"