bot is now a constant.
authorberghofe
Wed Jul 11 11:25:21 2007 +0200 (2007-07-11)
changeset 2375215839159f8b6
parent 23751 a7c7edf2c5ad
child 23753 d74a16b84e05
bot is now a constant.
src/HOL/Library/Continuity.thy
     1.1 --- a/src/HOL/Library/Continuity.thy	Wed Jul 11 11:24:36 2007 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Wed Jul 11 11:25:21 2007 +0200
     1.3 @@ -19,10 +19,6 @@
     1.4    continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
     1.5    "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
     1.6  
     1.7 -abbreviation
     1.8 -  bot :: "'a::complete_lattice" where
     1.9 -  "bot \<equiv> Sup {}"
    1.10 -
    1.11  lemma SUP_nat_conv:
    1.12    "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
    1.13  apply(rule order_antisym)