New theorem subset_inj_onto

--- a/src/HOL/Fun.ML	Mon May 26 12:36:56 1997 +0200
+++ b/src/HOL/Fun.ML	Mon May 26 12:37:24 1997 +0200
@@ -96,6 +96,11 @@
 by (REPEAT (resolve_tac prems 1));
 qed "inj_onto_contraD";
 
+goalw Fun.thy [inj_onto_def]
+    "!!A B. [| A<=B; inj_onto f B |] ==> inj_onto f A";
+by (Blast_tac 1);
+qed "subset_inj_onto";
+
 
 (*** Lemmas about inj ***)