# HG changeset patch
# User paulson
# Date 860145499 -7200
# Node ID f27002fc531dff8bbbf4b98bf2d1239c26791180
# Parent  a86f3b5f3cc781cdb11eb1eb12d9edc02f1b36ca
Adds image_eqI instead of imageI, as the former is more general

diff -r a86f3b5f3cc7 -r f27002fc531d src/HOL/Fun.ML
--- 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]