src/HOL/Product_Type.thy
changeset 37765 26bdfb7b680b
parent 37751 89e16802b6cc
child 37808 e604e5f9bb6a
     1.1 --- a/src/HOL/Product_Type.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -829,7 +829,7 @@
     1.4  *}
     1.5  
     1.6  definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
     1.7 -  [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
     1.8 +  "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
     1.9  
    1.10  lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
    1.11    by (simp add: prod_fun_def)