diff -r 1aa23e9f2c87 -r 138f414f14cb src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Tue Jan 04 15:32:56 2011 -0800
+++ b/src/HOL/HOLCF/Pcpo.thy	Tue Jan 04 15:46:38 2011 -0800
@@ -175,9 +175,6 @@
 
 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
 
-context pcpo
-begin
-
 text {* useful lemmas about @{term \<bottom>} *}
 
 lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
@@ -192,20 +189,6 @@
 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
 by (simp only: eq_bottom_iff lub_below_iff)
 
-lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>"
-by (simp add: lub_eq_bottom_iff)
-
-lemma chain_UU_I_inverse: "\<forall>i::nat. Y i = \<bottom> \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom>"
-by simp
-
-lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) \<noteq> \<bottom> \<Longrightarrow> \<exists>i::nat. Y i \<noteq> \<bottom>"
-  by (blast intro: chain_UU_I_inverse)
-
-lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
-  by (blast intro: bottomI)
-
-end
-
 subsection {* Chain-finite and flat cpos *}
 
 text {* further useful classes for HOLCF domains *}