src/HOL/Relation.ML
changeset 4733 2c984ac036f5
parent 4673 59d80bacee62
child 4746 a5dcd7e4a37d
--- 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";