1.1 --- a/src/HOLCF/Up.thy	Sat Nov 27 12:55:12 2010 -0800
     1.2 +++ b/src/HOLCF/Up.thy	Sat Nov 27 13:12:10 2010 -0800
     1.3 @@ -111,7 +111,7 @@
     1.4    proof (rule up_chain_lemma)
     1.5      assume "\<forall>i. S i = Ibottom"
     1.6      hence "range (\<lambda>i. S i) <<| Ibottom"
     1.7 -      by (simp add: lub_const)
     1.8 +      by (simp add: is_lub_const)
     1.9      thus ?thesis ..
    1.10    next
    1.11      fix A :: "nat \<Rightarrow> 'a"
    1.12 @@ -160,7 +160,7 @@
    1.13      assume A: "\<forall>i. Iup (A i) = Y (i + k)"
    1.14      assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
    1.15      hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
    1.16 -      by (simp add: thelubI contlub_cfun_arg)
    1.17 +      by (simp add: lub_eqI contlub_cfun_arg)
    1.18      also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
    1.19        by (simp add: A)
    1.20      also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
    1.21 @@ -223,7 +223,7 @@
    1.22    assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
    1.23    | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
    1.24  apply (rule up_chain_lemma [OF Y])
    1.25 -apply (simp_all add: inst_up_pcpo up_def cont_Iup thelubI)
    1.26 +apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
    1.27  done
    1.28  
    1.29  lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"