--- a/src/HOL/MetisExamples/BigO.thy Wed Mar 19 14:25:59 2008 +0100
+++ b/src/HOL/MetisExamples/BigO.thy Wed Mar 19 18:10:23 2008 +0100
@@ -31,7 +31,7 @@
(*** 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))))
@@ -100,7 +100,7 @@
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))))
@@ -141,7 +141,7 @@
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))))
@@ -173,7 +173,7 @@
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))))
@@ -209,7 +209,7 @@
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)))}"