1.1 --- a/src/HOL/Complete_Lattice.thy	Sat Jul 16 21:53:50 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sat Jul 16 22:04:02 2011 +0200
     1.3 @@ -108,20 +108,6 @@
     1.4    with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
     1.5  qed
     1.6  
     1.7 -lemma top_le:
     1.8 -  "\<top> \<sqsubseteq> x \<Longrightarrow> x = \<top>"
     1.9 -  by (rule antisym) auto
    1.10 -
    1.11 -lemma le_bot:
    1.12 -  "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
    1.13 -  by (rule antisym) auto
    1.14 -
    1.15 -lemma not_less_bot [simp]: "\<not> (x \<sqsubset> \<bottom>)"
    1.16 -  using bot_least [of x] by (auto simp: le_less)
    1.17 -
    1.18 -lemma not_top_less [simp]: "\<not> (\<top> \<sqsubset> x)"
    1.19 -  using top_greatest [of x] by (auto simp: le_less)
    1.20 -
    1.21  lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
    1.22    using Sup_upper[of u A] by auto
    1.23