New theorem subset_inj_onto
authorpaulson
Mon May 26 12:37:24 1997 +0200 (1997-05-26)
changeset 334189fe22bf9f54
parent 3340 a886795c9dce
child 3342 ec3b55fcb165
New theorem subset_inj_onto
src/HOL/Fun.ML
     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