# HG changeset patch
# User huffman
# Date 1269326003 25200
# Node ID 3da8db225c93a0ebb1cfec71f3769014607dfda9
# Parent  384a31bd5425960b231cac2cb32ed1f461a6d7bd
use Pair instead of cpair in Fixrec_ex.thy

diff -r 384a31bd5425 -r 3da8db225c93 src/HOLCF/ex/Fixrec_ex.thy
--- a/src/HOLCF/ex/Fixrec_ex.thy	Mon Mar 22 23:33:02 2010 -0700
+++ b/src/HOLCF/ex/Fixrec_ex.thy	Mon Mar 22 23:33:23 2010 -0700
@@ -13,7 +13,7 @@
 text {*
   Fixrec patterns can mention any constructor defined by the domain
   package, as well as any of the following built-in constructors:
-  cpair, spair, sinl, sinr, up, ONE, TT, FF.
+  Pair, spair, sinl, sinr, up, ONE, TT, FF.
 *}
 
 text {* Typical usage is with lazy constructors. *}
@@ -50,7 +50,7 @@
 fixrec
   lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
 where
-  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
 | "lzip\<cdot>lNil\<cdot>lNil = lNil"
 
 text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
@@ -118,7 +118,7 @@
 fixrec (permissive)
   lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
 where
-  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
 | "lzip2\<cdot>xs\<cdot>ys = lNil"
 
 text {*
@@ -130,7 +130,7 @@
 text {* Simp rules can be generated later using @{text fixrec_simp}. *}
 
 lemma lzip2_simps [simp]:
-  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
   "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
   "lzip2\<cdot>lNil\<cdot>lNil = lNil"