# HG changeset patch
# User haftmann
# Date 1310578992 -7200
# Node ID 58791b75cf1f6d9908c731d7f1bc0e2a2c094ad6
# Parent  07f0650146f29495c23ee1b01957c04b251fbfbf
moved lemmas bot_less and less_top to classes bot and top respectively

diff -r 07f0650146f2 -r 58791b75cf1f src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Wed Jul 13 19:40:18 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Wed Jul 13 19:43:12 2011 +0200
@@ -392,15 +392,6 @@
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   by (fact Inf_union_distrib)
 
-lemma (in bounded_lattice_bot) bot_less:
-  -- {* FIXME: tighten classes bot, top to partial orders (uniqueness!), move lemmas there *}
-  "a \<noteq> bot \<longleftrightarrow> bot < a"
-  by (auto simp add: less_le_not_le intro!: antisym)
-
-lemma (in bounded_lattice_top) less_top:
-  "a \<noteq> top \<longleftrightarrow> a < top"
-  by (auto simp add: less_le_not_le intro!: antisym)
-
 lemma (in complete_lattice) Inf_top_conv [no_atp]:
   "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
   "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
diff -r 07f0650146f2 -r 58791b75cf1f 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 *}