src/HOL/Library/Continuity.thy
changeset 54257 5c7a3b6b05a9
parent 46508 ec9630fe9ca7
     1.1 --- a/src/HOL/Library/Continuity.thy	Tue Nov 05 05:48:08 2013 +0100
     1.2 +++ b/src/HOL/Library/Continuity.thy	Tue Nov 05 09:44:57 2013 +0100
     1.3 @@ -19,7 +19,8 @@
     1.4    "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
     1.5  
     1.6  lemma SUP_nat_conv:
     1.7 -  "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
     1.8 +  fixes M :: "nat \<Rightarrow> 'a::complete_lattice"
     1.9 +  shows "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
    1.10  apply(rule order_antisym)
    1.11   apply(rule SUP_least)
    1.12   apply(case_tac n)