remove not_up_less_UU [simp]
authorhuffman
Wed Jan 02 18:54:21 2008 +0100 (2008-01-02)
changeset 25785dbe118fe3180
parent 25784 71157f7e671e
child 25786 6b3c79acac1f
remove not_up_less_UU [simp]
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Up.thy	Wed Jan 02 18:29:03 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Wed Jan 02 18:54:21 2008 +0100
     1.3 @@ -226,8 +226,8 @@
     1.4  lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
     1.5  by (simp add: up_def cont_Iup inst_up_pcpo)
     1.6  
     1.7 -lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
     1.8 -by (simp add: eq_UU_iff [symmetric])
     1.9 +lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
    1.10 +by simp
    1.11  
    1.12  lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
    1.13  by (simp add: up_def cont_Iup)