Adds image_eqI instead of imageI, as the former is more general

--- a/src/HOL/Fun.ML	Fri Apr 04 11:17:05 1997 +0200
+++ b/src/HOL/Fun.ML	Fri Apr 04 11:18:19 1997 +0200
@@ -35,7 +35,7 @@
 by (REPEAT (ares_tac prems 1));
 qed "imageE";
 
-AddIs  [imageI]; 
+AddIs  [image_eqI];
 AddSEs [imageE]; 
 
 goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
@@ -59,6 +59,8 @@
 by (rtac (major RS imageE) 1);
 by (etac minor 1);
 qed "rangeE";
+
+
 (*** inj(f): f is a one-to-one function ***)
 
 val prems = goalw Fun.thy [inj_def]