src/HOLCF/Fixrec.thy
changeset 40046 ba2e41c8b725
parent 39807 19ddbededdd3
child 40322 707eb30e8a53
     1.1 --- a/src/HOLCF/Fixrec.thy	Wed Oct 20 17:25:22 2010 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Wed Oct 20 19:40:02 2010 -0700
     1.3 @@ -115,7 +115,7 @@
     1.4  definition
     1.5    match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
     1.6  where
     1.7 -  "match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
     1.8 +  "match_UU = (\<Lambda> x k. strict\<cdot>x\<cdot>fail)"
     1.9  
    1.10  definition
    1.11    match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"