1.1 --- a/src/HOL/Fun.ML	Sat Nov 01 12:58:08 1997 +0100
     1.2 +++ b/src/HOL/Fun.ML	Sat Nov 01 12:59:06 1997 +0100
     1.3 @@ -128,5 +128,23 @@
     1.4                        addEs [inv_injective,injD]) 1);
     1.5  qed "inj_onto_inv";
     1.6  
     1.7 +goalw thy [inj_onto_def]
     1.8 +   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
     1.9 +by (Blast_tac 1);
    1.10 +qed "inj_onto_image_Int";
    1.11 +
    1.12 +goalw thy [inj_onto_def]
    1.13 +   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
    1.14 +by (Blast_tac 1);
    1.15 +qed "inj_onto_image_set_diff";
    1.16 +
    1.17 +goalw thy [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
    1.18 +by (Blast_tac 1);
    1.19 +qed "image_Int";
    1.20 +
    1.21 +goalw thy [inj_def] "!!f. inj f ==> f``(A-B) = f``A - f``B";
    1.22 +by (Blast_tac 1);
    1.23 +qed "image_set_diff";
    1.24 +
    1.25  
    1.26  val set_cs = !claset delrules [equalityI];