# HG changeset patch
# User huffman
# Date 1285891585 25200
# Node ID 19ddbededdd3c37eb0893476932004bff0b63368
# Parent  d59b9531d6b06adced5adb169a218bea0d9ddd76
fixrec: rename match_cpair to match_Pair

diff -r d59b9531d6b0 -r 19ddbededdd3 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed Sep 15 13:26:21 2010 -0700
+++ b/src/HOLCF/Fixrec.thy	Thu Sep 30 17:06:25 2010 -0700
@@ -118,9 +118,9 @@
   "match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
 
 definition
-  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
+  match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
 where
-  "match_cpair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
+  "match_Pair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
 
 definition
   match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
@@ -162,9 +162,9 @@
   "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
 by (simp_all add: match_UU_def)
 
-lemma match_cpair_simps [simp]:
-  "match_cpair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
-by (simp_all add: match_cpair_def)
+lemma match_Pair_simps [simp]:
+  "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
+by (simp_all add: match_Pair_def)
 
 lemma match_spair_simps [simp]:
   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y"
@@ -248,7 +248,7 @@
       (@{const_name sinl}, @{const_name match_sinl}),
       (@{const_name sinr}, @{const_name match_sinr}),
       (@{const_name spair}, @{const_name match_spair}),
-      (@{const_name Pair}, @{const_name match_cpair}),
+      (@{const_name Pair}, @{const_name match_Pair}),
       (@{const_name ONE}, @{const_name match_ONE}),
       (@{const_name TT}, @{const_name match_TT}),
       (@{const_name FF}, @{const_name match_FF}),