--- a/src/HOLCF/Up.thy Wed Jan 02 18:29:03 2008 +0100
+++ b/src/HOLCF/Up.thy Wed Jan 02 18:54:21 2008 +0100
@@ -226,8 +226,8 @@
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
by (simp add: up_def cont_Iup inst_up_pcpo)
-lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
-by (simp add: eq_UU_iff [symmetric])
+lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
+by simp
lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
by (simp add: up_def cont_Iup)