src/HOL/HOLCF/Fixrec.thy
changeset 40795 c52cd8bc426d
parent 40774 0437dbc127b3
child 40834 a1249aeff5b6
     1.1 --- a/src/HOL/HOLCF/Fixrec.thy	Sat Nov 27 22:48:08 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Sun Nov 28 07:29:32 2010 -0800
     1.3 @@ -150,9 +150,8 @@
     1.4    "match_FF = (\<Lambda> x k. If x then fail else k)"
     1.5  
     1.6  lemma match_bottom_simps [simp]:
     1.7 -  "match_bottom\<cdot>\<bottom>\<cdot>k = \<bottom>"
     1.8 -  "x \<noteq> \<bottom> \<Longrightarrow> match_bottom\<cdot>x\<cdot>k = fail"
     1.9 -by (simp_all add: match_bottom_def)
    1.10 +  "match_bottom\<cdot>x\<cdot>k = (if x = \<bottom> then \<bottom> else fail)"
    1.11 +by (simp add: match_bottom_def)
    1.12  
    1.13  lemma match_Pair_simps [simp]:
    1.14    "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"