src/HOL/Set.ML

--- a/src/HOL/Set.ML	Fri Jan 02 17:15:19 1998 +0100
+++ b/src/HOL/Set.ML	Fri Jan 02 17:15:52 1998 +0100
@@ -608,10 +608,14 @@
 by (Blast_tac 1);
 qed "image_Un";
 
-goal Set.thy "(z : f``A) = (EX x:A. z = f x)";
+goal thy "(z : f``A) = (EX x:A. z = f x)";
 by (Blast_tac 1);
 qed "image_iff";
 
+val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
+by (blast_tac (claset() addIs prems) 1);
+qed "image_subsetI";
+
 
 (*** Range of a function -- just a translation for image! ***)