src/HOL/Product_Type.thy
changeset 40702 cf26dd7395e4
parent 40607 30d512bf47a7
child 40929 7ff03a5e044f
--- a/src/HOL/Product_Type.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Product_Type.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -1135,6 +1135,7 @@
 qed
 
 lemma map_pair_surj:
+  fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd"
   assumes "surj f" and "surj g"
   shows "surj (map_pair f g)"
 unfolding surj_def