src/HOL/Library/BigO.thy
changeset 61762 d50b993b4fb9
parent 61585 a9599d3d7610
child 61945 1135b8de26c3
     1.1 --- a/src/HOL/Library/BigO.thy	Mon Nov 30 14:24:51 2015 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Tue Dec 01 14:09:10 2015 +0000
     1.3 @@ -200,8 +200,6 @@
     1.4    apply (auto simp add: fun_Compl_def func_plus)
     1.5    apply (drule_tac x = x in spec)+
     1.6    apply force
     1.7 -  apply (drule_tac x = x in spec)+
     1.8 -  apply force
     1.9    done
    1.10  
    1.11  lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"