--- a/src/HOL/MetisExamples/BigO.thy Mon Jul 16 19:11:37 2007 +0200
+++ b/src/HOL/MetisExamples/BigO.thy Mon Jul 16 19:18:23 2007 +0200
@@ -1343,13 +1343,10 @@
apply (rule_tac x = c in exI)
apply safe
apply (case_tac "x = 0")
-prefer 2
+apply (metis OrderedGroup.abs_ge_zero OrderedGroup.abs_zero order_less_le Ring_and_Field.split_mult_pos_le)
apply (subgoal_tac "x = Suc (x - 1)")
- apply (erule ssubst) back
- apply (erule spec)
- apply (rule Suc_pred')
+ apply metis
apply simp
-apply (metis OrderedGroup.abs_ge_zero OrderedGroup.abs_zero order_less_le Ring_and_Field.split_mult_pos_le)
done