changeset 22998 | 97e1f9c2cc46 |
parent 22974 | 08b0fa905ea0 |
child 23127 | 56ee8105c002 |
--- a/src/HOL/Hyperreal/SEQ.thy Thu May 17 19:49:40 2007 +0200 +++ b/src/HOL/Hyperreal/SEQ.thy Thu May 17 21:51:32 2007 +0200 @@ -725,7 +725,7 @@ lemma Bseq_isUb: "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U" -by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff) +by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) text{* Use completeness of reals (supremum property)