diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Order.thy
--- a/src/ZF/Order.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Order.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -25,17 +25,17 @@
 
   well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
 
-  mono_map_def "mono_map(A,r,B,s) == \
-\                   {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
+  mono_map_def "mono_map(A,r,B,s) == 
+                   {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
 
-  ord_iso_def  "ord_iso(A,r,B,s) == \
-\                   {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
+  ord_iso_def  "ord_iso(A,r,B,s) == 
+                   {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
 
   pred_def     "pred(A,x,r) == {y:A. <y,x>:r}"
 
   ord_iso_map_def
-     "ord_iso_map(A,r,B,s) == \
-\       UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).   \
-\            {<x,y>}"
+     "ord_iso_map(A,r,B,s) == 
+       UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).   
+            {<x,y>}"
 
 end