src/HOLCF/Up.thy
 changeset 16326 50a613925c4e parent 16319 1ff2965cc2e7 child 16553 aa36d41e4263
```     1.1 --- a/src/HOLCF/Up.thy	Wed Jun 08 16:11:09 2005 +0200
1.2 +++ b/src/HOLCF/Up.thy	Wed Jun 08 23:43:19 2005 +0200
1.3 @@ -285,7 +285,7 @@
1.4  lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
1.5  by (simp add: up_def cont_Iup)
1.6
1.7 -lemma up_eq: "(up\<cdot>x = up\<cdot>y) = (x = y)"
1.8 +lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
1.9  by (rule iffI, erule up_inject, simp)
1.10
1.11  lemma up_defined [simp]: " up\<cdot>x \<noteq> \<bottom>"
1.12 @@ -294,7 +294,7 @@
1.13  lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
1.14  by (simp add: eq_UU_iff [symmetric])
1.15
1.16 -lemma up_less: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
1.17 +lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
1.18  by (simp add: up_def cont_Iup)
1.19
1.20  lemma upE1: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
```