| changeset 30649 | 57753e0ec1d4 |
| parent 30082 | 43c5b7bfc791 |
| child 31017 | 2c227493ea56 |
--- a/src/HOL/Series.thy Sat Mar 21 12:37:13 2009 +0100 +++ b/src/HOL/Series.thy Sun Mar 22 19:36:04 2009 +0100 @@ -557,7 +557,6 @@ apply (induct_tac "na", auto) apply (rule_tac y = "c * norm (f (N + n))" in order_trans) apply (auto intro: mult_right_mono simp add: summable_def) -apply (simp add: mult_ac) apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI) apply (rule sums_divide) apply (rule sums_mult)