src/HOL/Fun.ML
changeset 6301 08245f5a436d
parent 6290 31483ca40e91
child 6829 50459a995aa3
     1.1 --- a/src/HOL/Fun.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/Fun.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -213,6 +213,14 @@
     1.4  by Auto_tac;
     1.5  qed "inv_image_comp";
     1.6  
     1.7 +Goal "inj f ==> (f a : f``A) = (a : A)";
     1.8 +by (blast_tac (claset() addDs [injD]) 1);
     1.9 +qed "inj_image_mem_iff";
    1.10 +
    1.11 +Goal "inj f ==> (f``A = f``B) = (A = B)";
    1.12 +by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
    1.13 +qed "inj_image_eq_iff";
    1.14 +
    1.15  val set_cs = claset() delrules [equalityI];
    1.16  
    1.17