src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Wed Jul 13 19:40:18 2011 +0200
+++ b/src/HOL/Orderings.thy	Wed Jul 13 19:43:12 2011 +0200
@@ -1086,10 +1086,24 @@
 class bot = order +
   fixes bot :: 'a
   assumes bot_least [simp]: "bot \<le> x"
+begin
+
+lemma bot_less:
+  "a \<noteq> bot \<longleftrightarrow> bot < a"
+  by (auto simp add: less_le_not_le intro!: antisym)
+
+end
 
 class top = order +
   fixes top :: 'a
   assumes top_greatest [simp]: "x \<le> top"
+begin
+
+lemma less_top:
+  "a \<noteq> top \<longleftrightarrow> a < top"
+  by (auto simp add: less_le_not_le intro!: antisym)
+
+end
 
 
 subsection {* Dense orders *}