changeset 60867 | 86e7560e07d0 |
parent 60758 | d8d85a8172b5 |
child 61531 | ab2e862263e7 |
--- a/src/HOL/Series.thy Thu Aug 06 19:12:09 2015 +0200 +++ b/src/HOL/Series.thy Thu Aug 06 23:56:48 2015 +0200 @@ -550,7 +550,7 @@ fix n show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n" using r r0 M [of n] - apply (auto simp add: abs_mult field_simps power_divide) + apply (auto simp add: abs_mult field_simps) apply (cases "r=0", simp) apply (cases n, auto) done