new theorem rev_image_eqI

--- a/src/HOL/Set.ML	Mon Nov 22 12:10:27 1999 +0100
+++ b/src/HOL/Set.ML	Tue Nov 23 11:18:19 1999 +0100
@@ -650,6 +650,11 @@
 
 bind_thm ("imageI", refl RS image_eqI);
 
+(*This version's more effective when we already have the required x*)
+Goalw [image_def] "[| x:A;  b=f(x) |] ==> b : f``A";
+by (Blast_tac 1);
+qed "rev_image_eqI";
+
 (*The eta-expansion gives variable-name preservation.*)
 val major::prems = Goalw [image_def]
     "[| b : (%x. f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P";