# 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 \ 'a::complete_lattice) \ bool" where "continuous F \ (\M. chain M \ F (SUP i. M i) = (SUP i. F (M i)))" -abbreviation - bot :: "'a::complete_lattice" where - "bot \ Sup {}" - lemma SUP_nat_conv: "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))" apply(rule order_antisym)