--- a/src/HOLCF/One.thy Fri Apr 10 11:35:21 2009 -0700
+++ b/src/HOLCF/One.thy Fri Apr 10 17:39:53 2009 -0700
@@ -37,8 +37,8 @@
lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
by (induct x rule: one_induct) simp_all
-lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE"
-unfolding ONE_def by simp_all
+lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
+unfolding ONE_def by simp
lemma one_neq_iffs [simp]:
"x \<noteq> ONE \<longleftrightarrow> x = \<bottom>"