bot is now a constant.

--- a/src/HOL/Library/Continuity.thy	Wed Jul 11 11:24:36 2007 +0200
+++ b/src/HOL/Library/Continuity.thy	Wed Jul 11 11:25:21 2007 +0200
@@ -19,10 +19,6 @@
   continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
   "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
 
-abbreviation
-  bot :: "'a::complete_lattice" where
-  "bot \<equiv> Sup {}"
-
 lemma SUP_nat_conv:
   "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
 apply(rule order_antisym)