src/HOLCF/Up.thy
changeset 26027 87cb69d27558
parent 25922 cb04d05e95fb
child 26046 1624b3304bb9
     1.1 --- a/src/HOLCF/Up.thy	Thu Jan 31 21:37:20 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Thu Jan 31 21:48:14 2008 +0100
     1.3 @@ -148,7 +148,7 @@
     1.4  apply assumption
     1.5  apply (subst up_lemma5, assumption+)
     1.6  apply (rule is_lub_Iup)
     1.7 -apply (rule thelubE [OF _ refl])
     1.8 +apply (rule cpo_lubI)
     1.9  apply (erule (1) up_lemma4)
    1.10  done
    1.11  
    1.12 @@ -170,7 +170,7 @@
    1.13  apply (frule up_chain_lemma, safe)
    1.14  apply (rule_tac x="Iup (lub (range A))" in exI)
    1.15  apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
    1.16 -apply (simp add: is_lub_Iup thelubE)
    1.17 +apply (simp add: is_lub_Iup cpo_lubI)
    1.18  apply (rule exI, rule lub_const)
    1.19  done
    1.20  
    1.21 @@ -198,7 +198,7 @@
    1.22  lemma cont_Iup: "cont Iup"
    1.23  apply (rule contI)
    1.24  apply (rule is_lub_Iup)
    1.25 -apply (erule thelubE [OF _ refl])
    1.26 +apply (erule cpo_lubI)
    1.27  done
    1.28  
    1.29  text {* continuity for @{term Ifup} *}