src/HOL/Library/BigO.thy
changeset 57418 6ab1c7cb0b8d
parent 56796 9f84219715a7
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -641,7 +641,8 @@
     1.4    apply (erule ssubst)
     1.5    apply (erule bigo_setsum3)
     1.6    apply (rule ext)
     1.7 -  apply (rule setsum_cong2)
     1.8 +  apply (rule setsum.cong)
     1.9 +  apply (rule refl)
    1.10    apply (subst abs_of_nonneg)
    1.11    apply auto
    1.12    done