# HG changeset patch
# User huffman
# Date 1290889677 28800
# Node ID 50a80cf4b7efbc56443daa32302d0e56fcd33c63
# Parent  a3e505b236e76399d9da8e068e5a3308441d2655
rename function 'match_UU' to 'match_bottom'

diff -r a3e505b236e7 -r 50a80cf4b7ef src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sat Nov 27 12:26:18 2010 -0800
+++ b/src/HOLCF/Fixrec.thy	Sat Nov 27 12:27:57 2010 -0800
@@ -105,9 +105,9 @@
 default_sort pcpo
 
 definition
-  match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
+  match_bottom :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
 where
-  "match_UU = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
+  "match_bottom = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
 
 definition
   match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
@@ -149,10 +149,10 @@
 where
   "match_FF = (\<Lambda> x k. If x then fail else k)"
 
-lemma match_UU_simps [simp]:
-  "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
-  "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
-by (simp_all add: match_UU_def)
+lemma match_bottom_simps [simp]:
+  "match_bottom\<cdot>\<bottom>\<cdot>k = \<bottom>"
+  "x \<noteq> \<bottom> \<Longrightarrow> match_bottom\<cdot>x\<cdot>k = fail"
+by (simp_all add: match_bottom_def)
 
 lemma match_Pair_simps [simp]:
   "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
@@ -244,7 +244,7 @@
       (@{const_name ONE}, @{const_name match_ONE}),
       (@{const_name TT}, @{const_name match_TT}),
       (@{const_name FF}, @{const_name match_FF}),
-      (@{const_name UU}, @{const_name match_UU}) ]
+      (@{const_name UU}, @{const_name match_bottom}) ]
 *}
 
 hide_const (open) succeed fail run