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