# 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 \ 'c match \ 'c match" + match_bottom :: "'a \ 'c match \ 'c match" where - "match_UU = (\ x k. seq\x\fail)" + "match_bottom = (\ x k. seq\x\fail)" definition match_Pair :: "'a::cpo \ 'b::cpo \ ('a \ 'b \ 'c match) \ 'c match" @@ -149,10 +149,10 @@ where "match_FF = (\ x k. If x then fail else k)" -lemma match_UU_simps [simp]: - "match_UU\\\k = \" - "x \ \ \ match_UU\x\k = fail" -by (simp_all add: match_UU_def) +lemma match_bottom_simps [simp]: + "match_bottom\\\k = \" + "x \ \ \ match_bottom\x\k = fail" +by (simp_all add: match_bottom_def) lemma match_Pair_simps [simp]: "match_Pair\(x, y)\k = k\x\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