# HG changeset patch
# User berghofe
# Date 1184145921 -7200
# Node ID 15839159f8b6e11fe26eec724fe32a910c4f49c2
# Parent  a7c7edf2c5ad5e9b52e2e6ef074b7419aaead15c
bot is now a constant.

diff -r a7c7edf2c5ad -r 15839159f8b6 src/HOL/Library/Continuity.thy
--- 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)