1.1 --- a/src/HOLCF/Fixrec.thy Sat Nov 27 12:26:18 2010 -0800
1.2 +++ b/src/HOLCF/Fixrec.thy Sat Nov 27 12:27:57 2010 -0800
1.3 @@ -105,9 +105,9 @@
1.4 default_sort pcpo
1.5
1.6 definition
1.7 - match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
1.8 + match_bottom :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
1.9 where
1.10 - "match_UU = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
1.11 + "match_bottom = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
1.12
1.13 definition
1.14 match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
1.15 @@ -149,10 +149,10 @@
1.16 where
1.17 "match_FF = (\<Lambda> x k. If x then fail else k)"
1.18
1.19 -lemma match_UU_simps [simp]:
1.20 - "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
1.21 - "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
1.22 -by (simp_all add: match_UU_def)
1.23 +lemma match_bottom_simps [simp]:
1.24 + "match_bottom\<cdot>\<bottom>\<cdot>k = \<bottom>"
1.25 + "x \<noteq> \<bottom> \<Longrightarrow> match_bottom\<cdot>x\<cdot>k = fail"
1.26 +by (simp_all add: match_bottom_def)
1.27
1.28 lemma match_Pair_simps [simp]:
1.29 "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
1.30 @@ -244,7 +244,7 @@
1.31 (@{const_name ONE}, @{const_name match_ONE}),
1.32 (@{const_name TT}, @{const_name match_TT}),
1.33 (@{const_name FF}, @{const_name match_FF}),
1.34 - (@{const_name UU}, @{const_name match_UU}) ]
1.35 + (@{const_name UU}, @{const_name match_bottom}) ]
1.36 *}
1.37
1.38 hide_const (open) succeed fail run