src/HOL/Library/Continuity.thy
changeset 23752 15839159f8b6
parent 22452 8a86fd2a1bf0
child 24331 76f7a8c6e842
     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)