| changeset 15085 | 5693a977a767 |
| parent 15082 | 6c3276a2735b |
| child 15102 | 04b0e943fcc9 |
--- a/src/HOL/Hyperreal/SEQ.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Hyperreal/SEQ.thy Thu Jul 29 16:14:42 2004 +0200 @@ -796,7 +796,7 @@ apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI) apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI) apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI) -apply (auto elim!: lemma_Nat_covered, arith+) +apply (auto elim!: lemma_Nat_covered) done text{*A Cauchy sequence is bounded -- nonstandard version*}