diff -r 5a6f2aabd538 -r 6bcb44e4d6e5 src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/domrange.ML	Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	ZF/domrange
+(*  Title:      ZF/domrange
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
 Converse, domain, range of a relation or function
@@ -31,7 +31,7 @@
     (assume_tac 1) ]);
 
 val converse_cs = pair_cs addSIs [converseI] 
-			  addSEs [converseD,converseE];
+                          addSEs [converseD,converseE];
 
 qed_goal "converse_converse" ZF.thy
     "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
@@ -137,7 +137,7 @@
 qed_goal "image_singleton_iff" ZF.thy
     "b : r``{a} <-> <a,b>:r"
  (fn _ => [ rtac (image_iff RS iff_trans) 1,
-	    fast_tac pair_cs 1 ]);
+            fast_tac pair_cs 1 ]);
 
 qed_goalw "imageI" ZF.thy [image_def]
     "!!a b r. [| <a,b>: r;  a:A |] ==> b : r``A"
@@ -163,7 +163,7 @@
 qed_goal "vimage_singleton_iff" ZF.thy
     "a : r-``{b} <-> <a,b>:r"
  (fn _ => [ rtac (vimage_iff RS iff_trans) 1,
-	    fast_tac pair_cs 1 ]);
+            fast_tac pair_cs 1 ]);
 
 qed_goalw "vimageI" ZF.thy [vimage_def]
     "!!A B r. [| <a,b>: r;  b:B |] ==> a : r-``B"