define cprod_fun using Pair instead of cpair
authorhuffman
Mon, 02 Nov 2009 17:29:34 -0800
changeset 33400 7c4ab69a15c3
parent 33399 768b2bb9e66a
child 33401 fc43fa403a69
define cprod_fun using Pair instead of cpair
src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Mon Nov 02 17:19:49 2009 -0800
+++ b/src/HOLCF/Domain.thy	Mon Nov 02 17:29:34 2009 -0800
@@ -222,7 +222,7 @@
 definition
   cprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
 where
-  "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. <f\<cdot>x, g\<cdot>y>))"
+  "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. (f\<cdot>x, g\<cdot>y)))"
 
 definition
   u_fun :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"