src/HOL/Relation.ML
changeset 1465 5d7a7e439cec
parent 1454 d0266c81a85e
child 1552 6f71b5d46700
--- a/src/HOL/Relation.ML	Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/Relation.ML	Tue Jan 30 15:24:36 1996 +0100
@@ -1,7 +1,7 @@
-(*  Title: 	Relation.ML
+(*  Title:      Relation.ML
     ID:         $Id$
-    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
-        	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
+                Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994 Universita' di Firenze
     Copyright   1993  University of Cambridge
 *)
@@ -100,7 +100,7 @@
     (assume_tac 1) ]);
 
 val converse_cs = comp_cs addSIs [converseI] 
-			  addSEs [converseD,converseE];
+                          addSEs [converseD,converseE];
 
 (** Domain **)
 
@@ -138,13 +138,13 @@
 qed_goal "Image_singleton_iff" Relation.thy
     "(b : r^^{a}) = ((a,b):r)"
  (fn _ => [ rtac (Image_iff RS trans) 1,
-	    fast_tac comp_cs 1 ]);
+            fast_tac comp_cs 1 ]);
 
 qed_goalw "ImageI" Relation.thy [Image_def]
     "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
  (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
             (resolve_tac [conjI ] 1),
-            (resolve_tac [RangeI] 1),
+            (rtac RangeI 1),
             (REPEAT (fast_tac set_cs 1))]);
 
 qed_goalw "ImageE" Relation.thy [Image_def]