src/HOL/Library/BigO.thy
changeset 56544 b60d5d119489
parent 56541 0e3abadbef39
child 56796 9f84219715a7
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Apr 11 23:22:00 2014 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Sat Apr 12 17:26:27 2014 +0200
     1.3 @@ -62,8 +62,7 @@
     1.4    apply (auto simp add: bigo_alt_def)
     1.5    apply (rule_tac x = "ca * c" in exI)
     1.6    apply (rule conjI)
     1.7 -  apply (rule mult_pos_pos)
     1.8 -  apply assumption+
     1.9 +  apply simp
    1.10    apply (rule allI)
    1.11    apply (drule_tac x = "xa" in spec)+
    1.12    apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")