src/HOLCF/One.thy
changeset 31076 99fe356cbbc2
parent 30911 7809cbaa1b61
child 35431 8758fe1fc9f8
     1.1 --- a/src/HOLCF/One.thy	Fri May 08 19:28:11 2009 +0100
     1.2 +++ b/src/HOLCF/One.thy	Fri May 08 16:19:51 2009 -0700
     1.3 @@ -28,13 +28,13 @@
     1.4  lemma one_induct: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
     1.5  by (cases x rule: oneE) simp_all
     1.6  
     1.7 -lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
     1.8 +lemma dist_below_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
     1.9  unfolding ONE_def by simp
    1.10  
    1.11 -lemma less_ONE [simp]: "x \<sqsubseteq> ONE"
    1.12 +lemma below_ONE [simp]: "x \<sqsubseteq> ONE"
    1.13  by (induct x rule: one_induct) simp_all
    1.14  
    1.15 -lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
    1.16 +lemma ONE_below_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
    1.17  by (induct x rule: one_induct) simp_all
    1.18  
    1.19  lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"