src/HOL/Hyperreal/SEQ.thy

--- 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)