1.1 --- a/src/HOL/Complete_Lattice.thy	Wed Jul 13 19:40:18 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Wed Jul 13 19:43:12 2011 +0200
     1.3 @@ -392,15 +392,6 @@
     1.4  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
     1.5    by (fact Inf_union_distrib)
     1.6  
     1.7 -lemma (in bounded_lattice_bot) bot_less:
     1.8 -  -- {* FIXME: tighten classes bot, top to partial orders (uniqueness!), move lemmas there *}
     1.9 -  "a \<noteq> bot \<longleftrightarrow> bot < a"
    1.10 -  by (auto simp add: less_le_not_le intro!: antisym)
    1.11 -
    1.12 -lemma (in bounded_lattice_top) less_top:
    1.13 -  "a \<noteq> top \<longleftrightarrow> a < top"
    1.14 -  by (auto simp add: less_le_not_le intro!: antisym)
    1.15 -
    1.16  lemma (in complete_lattice) Inf_top_conv [no_atp]:
    1.17    "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
    1.18    "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"