src/HOL/Library/BigO.thy
changeset 60142 3275dddf356f
parent 60141 833adf7db7d8
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/BigO.thy	Tue Apr 21 17:19:00 2015 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Wed Apr 22 12:43:06 2015 +0100
     1.3 @@ -870,7 +870,7 @@
     1.4    apply (drule bigo_LIMSEQ1)
     1.5    apply assumption
     1.6    apply (simp only: fun_diff_def)
     1.7 -  apply (erule Lim_transform)
     1.8 +  apply (erule Lim_transform2)
     1.9    apply assumption
    1.10    done
    1.11