src/HOLCF/Cfun.thy
changeset 25723 80c06e4d4db6
parent 25701 73fbe868b4e7
child 25786 6b3c79acac1f
     1.1 --- a/src/HOLCF/Cfun.thy	Thu Dec 20 01:07:21 2007 +0100
     1.2 +++ b/src/HOLCF/Cfun.thy	Thu Dec 20 03:06:20 2007 +0100
     1.3 @@ -496,9 +496,7 @@
     1.4  done
     1.5  
     1.6  (*FIXME: long proof*)
     1.7 -lemma contlub_strictify2:
     1.8 -  fixes f :: "'a::pcpo \<rightarrow> 'b::pcpo"
     1.9 -  shows "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
    1.10 +lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
    1.11  apply (rule contlubI)
    1.12  apply (case_tac "lub (range Y) = \<bottom>")
    1.13  apply (drule (1) chain_UU_I)