fixrec: rename match_cpair to match_Pair
authorhuffman
Thu Sep 30 17:06:25 2010 -0700 (2010-09-30)
changeset 3980719ddbededdd3
parent 39806 d59b9531d6b0
child 39808 1410c84013b9
fixrec: rename match_cpair to match_Pair
src/HOLCF/Fixrec.thy
     1.1 --- a/src/HOLCF/Fixrec.thy	Wed Sep 15 13:26:21 2010 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Thu Sep 30 17:06:25 2010 -0700
     1.3 @@ -118,9 +118,9 @@
     1.4    "match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
     1.5  
     1.6  definition
     1.7 -  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
     1.8 +  match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
     1.9  where
    1.10 -  "match_cpair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
    1.11 +  "match_Pair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
    1.12  
    1.13  definition
    1.14    match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
    1.15 @@ -162,9 +162,9 @@
    1.16    "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
    1.17  by (simp_all add: match_UU_def)
    1.18  
    1.19 -lemma match_cpair_simps [simp]:
    1.20 -  "match_cpair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
    1.21 -by (simp_all add: match_cpair_def)
    1.22 +lemma match_Pair_simps [simp]:
    1.23 +  "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
    1.24 +by (simp_all add: match_Pair_def)
    1.25  
    1.26  lemma match_spair_simps [simp]:
    1.27    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y"
    1.28 @@ -248,7 +248,7 @@
    1.29        (@{const_name sinl}, @{const_name match_sinl}),
    1.30        (@{const_name sinr}, @{const_name match_sinr}),
    1.31        (@{const_name spair}, @{const_name match_spair}),
    1.32 -      (@{const_name Pair}, @{const_name match_cpair}),
    1.33 +      (@{const_name Pair}, @{const_name match_Pair}),
    1.34        (@{const_name ONE}, @{const_name match_ONE}),
    1.35        (@{const_name TT}, @{const_name match_TT}),
    1.36        (@{const_name FF}, @{const_name match_FF}),