# HG changeset patch
# User paulson
# Date 1184606303 -7200
# Node ID 3879cb3d0ba7c5abdcbb966d17403d01b26c6e63
# Parent  73dbab55d28313ddd1de69e0d5467cd5268ddc10
tidied using sledgehammer

diff -r 73dbab55d283 -r 3879cb3d0ba7 src/HOL/MetisExamples/BigO.thy
--- 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