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