# HG changeset patch
# User paulson
# Date 910795755 -3600
# Node ID 17c869f24c5f1fde28f1adabfa4414490b540168
# Parent  d99feda2d2267fa3b9b8eab1445485a6bd415856
proved surjI

diff -r d99feda2d226 -r 17c869f24c5f src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Nov 11 15:45:32 1998 +0100
+++ b/src/HOL/Fun.ML	Wed Nov 11 15:49:15 1998 +0100
@@ -180,6 +180,12 @@
 qed "image_set_diff";
 
 
+
+val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
+by (blast_tac (claset() addIs [major RS sym]) 1);
+qed "surjI";
+
+
 val set_cs = claset() delrules [equalityI];