src/HOL/Fun.ML
changeset 3341 89fe22bf9f54
parent 2935 998cb95fdd43
child 3842 b55686a7b22c
     1.1 --- a/src/HOL/Fun.ML	Mon May 26 12:36:56 1997 +0200
     1.2 +++ b/src/HOL/Fun.ML	Mon May 26 12:37:24 1997 +0200
     1.3 @@ -96,6 +96,11 @@
     1.4  by (REPEAT (resolve_tac prems 1));
     1.5  qed "inj_onto_contraD";
     1.6  
     1.7 +goalw Fun.thy [inj_onto_def]
     1.8 +    "!!A B. [| A<=B; inj_onto f B |] ==> inj_onto f A";
     1.9 +by (Blast_tac 1);
    1.10 +qed "subset_inj_onto";
    1.11 +
    1.12  
    1.13  (*** Lemmas about inj ***)
    1.14