src/HOLCF/LowerPD.thy
changeset 40321 d065b195ec89
parent 40002 c5b5f7a3a3b1
child 40327 1dfdbd66093a
--- a/src/HOLCF/LowerPD.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Wed Oct 27 13:54:18 2010 -0700
@@ -229,10 +229,10 @@
 using lower_unit_Rep_compact_basis [of compact_bot]
 by (simp add: inst_lower_pd_pcpo)
 
-lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma lower_unit_bottom_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
 unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
 
-lemma lower_plus_strict_iff [simp]:
+lemma lower_plus_bottom_iff [simp]:
   "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
 apply safe
 apply (rule UU_I, erule subst, rule lower_plus_below1)