Adds image_eqI instead of imageI, as the former is more general
authorpaulson
Fri Apr 04 11:18:19 1997 +0200 (1997-04-04)
changeset 2890f27002fc531d
parent 2889 a86f3b5f3cc7
child 2891 d8f254ad1ab9
Adds image_eqI instead of imageI, as the former is more general
src/HOL/Fun.ML
     1.1 --- a/src/HOL/Fun.ML	Fri Apr 04 11:17:05 1997 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri Apr 04 11:18:19 1997 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  by (REPEAT (ares_tac prems 1));
     1.5  qed "imageE";
     1.6  
     1.7 -AddIs  [imageI]; 
     1.8 +AddIs  [image_eqI];
     1.9  AddSEs [imageE]; 
    1.10  
    1.11  goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
    1.12 @@ -59,6 +59,8 @@
    1.13  by (rtac (major RS imageE) 1);
    1.14  by (etac minor 1);
    1.15  qed "rangeE";
    1.16 +
    1.17 +
    1.18  (*** inj(f): f is a one-to-one function ***)
    1.19  
    1.20  val prems = goalw Fun.thy [inj_def]