# HG changeset patch
# User paulson
# Date 997094439 -7200
# Node ID 1b6258b288ba2180b0640d9f1b429d127670bfe7
# Parent  09a6c44a48eaefa66ce35d700937b9f4a3d472eb
new result comp_surj

diff -r 09a6c44a48ea -r 1b6258b288ba src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Aug 03 18:04:55 2001 +0200
+++ b/src/HOL/Fun.ML	Mon Aug 06 12:40:39 2001 +0200
@@ -129,8 +129,9 @@
 by (blast_tac (claset() addSDs [inj_onD]) 1);
 qed "inj_on_iff";
 
-Goalw [o_def] "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
-by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
+Goalw [o_def, inj_on_def]
+     "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
+by (Blast_tac 1);
 qed "comp_inj_on";
 
 Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
@@ -161,6 +162,13 @@
 by (Blast_tac 1);
 qed "surjD";
 
+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); 
+by (Clarify_tac 1); 
+by (dres_inst_tac [("x","x")] spec 1); 
+by (Blast_tac 1); 
+qed "comp_surj";
 
 
 (** Bijections **)