# HG changeset patch
# User huffman
# Date 1199296461 -3600
# Node ID dbe118fe31808b3e52b85c8a2f6ac14499fa908f
# Parent  71157f7e671e9e794027fba204984a346434514e
remove not_up_less_UU [simp]

diff -r 71157f7e671e -r dbe118fe3180 src/HOLCF/Up.thy
--- 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)