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