changeset 22998 | 97e1f9c2cc46 |
parent 22654 | c2b6b5a9e136 |
child 23114 | 1bd84606b403 |
--- a/src/HOL/Hyperreal/Ln.thy Thu May 17 19:49:40 2007 +0200 +++ b/src/HOL/Hyperreal/Ln.thy Thu May 17 21:51:32 2007 +0200 @@ -113,7 +113,7 @@ proof - have "(%n. (1 / 2::real)^n) sums (1 / (1 - (1/2)))" apply (rule geometric_sums) - by (simp add: abs_interval_iff) + by (simp add: abs_less_iff) also have "(1::real) / (1 - 1/2) = 2" by simp finally have "(%n. (1 / 2::real)^n) sums 2" .