src/HOL/Library/BigO.thy
changeset 56541 0e3abadbef39
parent 56536 aefb4a8da31f
child 56544 b60d5d119489
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Apr 11 17:53:16 2014 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Fri Apr 11 22:53:33 2014 +0200
     1.3 @@ -851,8 +851,7 @@
     1.4    apply clarify
     1.5    apply (drule_tac x = "r / c" in spec)
     1.6    apply (drule mp)
     1.7 -  apply (erule divide_pos_pos)
     1.8 -  apply assumption
     1.9 +  apply simp
    1.10    apply clarify
    1.11    apply (rule_tac x = no in exI)
    1.12    apply (rule allI)