# HG changeset patch
# User paulson
# Date 864643044 -7200
# Node ID 89fe22bf9f546f646a9ac9dafd7cf0ca4af26668
# Parent  a886795c9dce097f8b548f0e932d476684ea5602
New theorem subset_inj_onto

diff -r a886795c9dce -r 89fe22bf9f54 src/HOL/Fun.ML
--- 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 ***)