src/HOLCF/Fixrec.thy
changeset 40322 707eb30e8a53
parent 40046 ba2e41c8b725
child 40327 1dfdbd66093a
     1.1 --- a/src/HOLCF/Fixrec.thy	Wed Oct 27 13:54:18 2010 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Wed Oct 27 14:15:54 2010 -0700
     1.3 @@ -150,12 +150,12 @@
     1.4  definition
     1.5    match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
     1.6  where
     1.7 -  "match_TT = (\<Lambda> x k. If x then k else fail fi)"
     1.8 +  "match_TT = (\<Lambda> x k. If x then k else fail)"
     1.9   
    1.10  definition
    1.11    match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
    1.12  where
    1.13 -  "match_FF = (\<Lambda> x k. If x then fail else k fi)"
    1.14 +  "match_FF = (\<Lambda> x k. If x then fail else k)"
    1.15  
    1.16  lemma match_UU_simps [simp]:
    1.17    "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"