# HG changeset patch
# User paulson
# Date 889610714 -3600
# Node ID 2c984ac036f5244d6caaab8b48e327f4d985a063
# Parent  10af4886b33fab89d5e727d66a7789725847467d
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image

diff -r 10af4886b33f -r 2c984ac036f5 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Wed Mar 11 11:03:43 1998 +0100
+++ b/src/HOL/Relation.ML	Wed Mar 11 11:05:14 1998 +0100
@@ -219,17 +219,15 @@
     "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "Image_Un" thy
-    "R ^^ (A Un B) = R ^^ A Un R ^^ B"
+qed_goal "Image_Un" thy "R ^^ (A Un B) = R ^^ A Un R ^^ B"
  (fn _ => [ Blast_tac 1 ]);
 
-
-qed_goal "Image_subset" thy
-    "!!A B r. r <= A Times B ==> r^^C <= B"
+qed_goal "Image_subset" thy "!!A B r. r <= A Times B ==> r^^C <= B"
  (fn _ =>
   [ (rtac subsetI 1),
     (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
 
-goal thy "f-``(r^-1 ^^ {x}) = (UN y: r^-1 ^^ {x}. f-``{y})";
+(*NOT suitable for rewriting*)
+goal thy "r^^B = (UN y: B. r^^{y})";
 by (Blast_tac 1);
-qed "vimage_inverse_Image";
+qed "Image_eq_UN";