# HG changeset patch
# User paulson
# Date 918553555 -3600
# Node ID a3098667b9b65e5d4fbcf3bf354b7f7d35b68cb5
# Parent  a5f9fa6b6d7c343dc2f952008d108e99bf1cff5a
new lemma surjD

diff -r a5f9fa6b6d7c -r a3098667b9b6 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Mon Feb 08 17:33:47 1999 +0100
+++ b/src/HOL/Fun.ML	Tue Feb 09 10:45:55 1999 +0100
@@ -142,14 +142,18 @@
 
 (** surj **)
 
-val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
-by (blast_tac (claset() addIs [major RS sym]) 1);
+val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
+by (blast_tac (claset() addIs [prem RS sym]) 1);
 qed "surjI";
 
 Goalw [surj_def] "surj f ==> range f = UNIV";
 by Auto_tac;
 qed "surj_range";
 
+Goalw [surj_def] "surj f ==> EX x. y = f x";
+by (Blast_tac 1);
+qed "surjD";
+
 
 (*** Lemmas about injective functions and inv ***)