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