src/HOL/HOLCF/One.thy

--- a/src/HOL/HOLCF/One.thy	Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/One.thy	Wed Dec 15 19:15:06 2010 -0800
@@ -28,7 +28,7 @@
 lemma one_induct [case_names bottom ONE]: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
 by (cases x rule: oneE) simp_all
 
-lemma dist_below_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
+lemma dist_below_one [simp]: "ONE \<notsqsubseteq> \<bottom>"
 unfolding ONE_def by simp
 
 lemma below_ONE [simp]: "x \<sqsubseteq> ONE"