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