--- a/src/HOL/Metis_Examples/Big_O.thy Thu Nov 17 05:27:45 2011 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Thu Nov 17 06:01:47 2011 +0100
@@ -215,7 +215,7 @@
apply (rule mult_left_mono)
apply (rule abs_triangle_ineq)
apply (simp add: order_less_le)
-apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
+apply (metis abs_not_less_zero even_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
done
lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"