# 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 ***)