1.1 --- a/src/HOL/Orderings.thy	Wed Jul 13 19:40:18 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Jul 13 19:43:12 2011 +0200
     1.3 @@ -1086,10 +1086,24 @@
     1.4  class bot = order +
     1.5    fixes bot :: 'a
     1.6    assumes bot_least [simp]: "bot \<le> x"
     1.7 +begin
     1.8 +
     1.9 +lemma bot_less:
    1.10 +  "a \<noteq> bot \<longleftrightarrow> bot < a"
    1.11 +  by (auto simp add: less_le_not_le intro!: antisym)
    1.12 +
    1.13 +end
    1.14  
    1.15  class top = order +
    1.16    fixes top :: 'a
    1.17    assumes top_greatest [simp]: "x \<le> top"
    1.18 +begin
    1.19 +
    1.20 +lemma less_top:
    1.21 +  "a \<noteq> top \<longleftrightarrow> a < top"
    1.22 +  by (auto simp add: less_le_not_le intro!: antisym)
    1.23 +
    1.24 +end
    1.25  
    1.26  
    1.27  subsection {* Dense orders *}