1.1 --- a/src/HOL/Relation.ML	Sat Nov 06 15:34:12 1999 +0100
     1.2 +++ b/src/HOL/Relation.ML	Thu Nov 11 10:24:14 1999 +0100
     1.3 @@ -309,7 +309,7 @@
     1.4  
     1.5  (*** Image of a set under a relation ***)
     1.6  
     1.7 -overload_1st_set "Relation.op ^^";
     1.8 +overload_1st_set "Relation.Image";
     1.9  
    1.10  Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
    1.11  by (Blast_tac 1);
    1.12 @@ -389,6 +389,9 @@
    1.13  by (Blast_tac 1);
    1.14  qed "Image_INT_subset";
    1.15  
    1.16 +Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))";
    1.17 +by (Blast_tac 1);
    1.18 +qed "Image_subset_eq";
    1.19  
    1.20  section "Univalent";
    1.21