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