--- a/src/HOL/Metis_Examples/BigO.thy Mon Apr 26 23:45:32 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Mon Apr 26 23:45:51 2010 +0200
@@ -26,9 +26,9 @@
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 ***)
+(*** Now various verions with an increasing shrink factor ***)
-sledgehammer_params [modulus = 1]
+sledgehammer_params [shrink_factor = 1]
lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -97,7 +97,7 @@
by (metis abs_le_iff 5 18 14)
qed
-sledgehammer_params [modulus = 2]
+sledgehammer_params [shrink_factor = 2]
lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -138,7 +138,7 @@
by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
qed
-sledgehammer_params [modulus = 3]
+sledgehammer_params [shrink_factor = 3]
lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -170,7 +170,7 @@
qed
-sledgehammer_params [modulus = 4]
+sledgehammer_params [shrink_factor = 4]
lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
--- a/src/HOL/Metis_Examples/set.thy Mon Apr 26 23:45:32 2010 +0200
+++ b/src/HOL/Metis_Examples/set.thy Mon Apr 26 23:45:51 2010 +0200
@@ -19,7 +19,7 @@
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
by metis
-sledgehammer_params [modulus = 1]
+sledgehammer_params [shrink_factor = 1]
(*multiple versions of this example*)
@@ -90,7 +90,7 @@
by (metis 31 29)
qed
-sledgehammer_params [modulus = 2]
+sledgehammer_params [shrink_factor = 2]
lemma (*equal_union: *)
"(X = Y \<union> Z) =
@@ -133,7 +133,7 @@
by (metis 18 17)
qed
-sledgehammer_params [modulus = 3]
+sledgehammer_params [shrink_factor = 3]
lemma (*equal_union: *)
"(X = Y \<union> Z) =
@@ -168,7 +168,7 @@
(*Example included in TPHOLs paper*)
-sledgehammer_params [modulus = 4]
+sledgehammer_params [shrink_factor = 4]
lemma (*equal_union: *)
"(X = Y \<union> Z) =