src/HOL/MetisExamples/BigO.thy

   apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult)
   done
 
 (*** Now various verions with an increasing modulus ***)
 
-declare [[reconstruction_modulus = 1]]
+declare [[sledgehammer_modulus = 1]]
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
   apply auto

   by (metis 17 3 15)
 show "False"
   by (metis abs_le_iff 5 18 14)
 qed
 
-declare [[reconstruction_modulus = 2]]
+declare [[sledgehammer_modulus = 2]]
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
   apply auto

   by (metis abs_ge_self xt1(6) abs_le_D1)
 show "False"
   by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
 qed
 
-declare [[reconstruction_modulus = 3]]
+declare [[sledgehammer_modulus = 3]]
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
   apply auto

 show "False"
   by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff)
 qed
 
 
-declare [[reconstruction_modulus = 1]]
+declare [[sledgehammer_modulus = 1]]
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
   apply auto

 show "False"
   by (metis 6 8 10 abs_leI)
 qed
 
 
-declare [[reconstruction_sorts = true]]
+declare [[sledgehammer_sorts = true]]
 
 lemma bigo_alt_def: "O(f) = 
     {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
 by (auto simp add: bigo_def bigo_pos_const)