Fixed obsolete use of "op ^^"; new lemma

--- a/src/HOL/Relation.ML	Sat Nov 06 15:34:12 1999 +0100
+++ b/src/HOL/Relation.ML	Thu Nov 11 10:24:14 1999 +0100
@@ -309,7 +309,7 @@
 
 (*** Image of a set under a relation ***)
 
-overload_1st_set "Relation.op ^^";
+overload_1st_set "Relation.Image";
 
 Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
 by (Blast_tac 1);
@@ -389,6 +389,9 @@
 by (Blast_tac 1);
 qed "Image_INT_subset";
 
+Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))";
+by (Blast_tac 1);
+qed "Image_subset_eq";
 
 section "Univalent";