src/HOL/HOLCF/Fixrec.thy
changeset 41029 f7d8cfa6e7fc
parent 40834 a1249aeff5b6
child 41429 cf5f025bc3c7
     1.1 --- a/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 08:43:52 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 08:59:58 2010 -0800
     1.3 @@ -36,10 +36,10 @@
     1.4  done
     1.5  
     1.6  lemma succeed_defined [simp]: "succeed\<cdot>x \<noteq> \<bottom>"
     1.7 -by (simp add: succeed_def cont_Abs_match Abs_match_defined)
     1.8 +by (simp add: succeed_def cont_Abs_match Abs_match_bottom_iff)
     1.9  
    1.10  lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
    1.11 -by (simp add: fail_def Abs_match_defined)
    1.12 +by (simp add: fail_def Abs_match_bottom_iff)
    1.13  
    1.14  lemma succeed_eq [simp]: "(succeed\<cdot>x = succeed\<cdot>y) = (x = y)"
    1.15  by (simp add: succeed_def cont_Abs_match Abs_match_inject)