# HG changeset patch
# User wenzelm
# Date 1001622128 -7200
# Node ID 9273cef990f5fb8fb44fa68a6d51ac78e29f0b04
# Parent  bbd6268e0b4b80e45094e177abf2b3be88b21db2
added surjE;

diff -r bbd6268e0b4b -r 9273cef990f5 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Thu Sep 27 18:56:39 2001 +0200
+++ b/src/HOL/Fun.ML	Thu Sep 27 22:22:08 2001 +0200
@@ -162,6 +162,13 @@
 by (Blast_tac 1);
 qed "surjD";
 
+val [p1, p2] = Goal "surj f ==> (!!x. y = f x ==> C) ==> C";
+by (cut_facts_tac [p1 RS surjD] 1);
+by (etac exE 1);
+by (rtac p2 1);
+by (atac 1);
+qed "surjE";
+
 Goalw [o_def, surj_def] "[| surj f;  surj g |] ==> surj (g o f)";
 by (Clarify_tac 1); 
 by (dres_inst_tac [("x","y")] spec 1);