src/HOL/Library/BigO.thy
changeset 19279 48b527d0331b
parent 17199 59c1bfc81d91
child 19736 d8d0f8f51d69
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Mar 17 09:57:25 2006 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Fri Mar 17 10:04:27 2006 +0100
     1.3 @@ -582,7 +582,7 @@
     1.4    apply (subst abs_of_nonneg) back back
     1.5    apply (rule setsum_nonneg)
     1.6    apply force
     1.7 -  apply (subst setsum_mult)
     1.8 +  apply (subst setsum_right_distrib)
     1.9    apply (rule allI)
    1.10    apply (rule order_trans)
    1.11    apply (rule setsum_abs)