--- a/src/HOL/Metis_Examples/BigO.thy Fri May 14 22:29:50 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Fri May 14 22:30:24 2010 +0200
@@ -28,7 +28,7 @@
(*** Now various verions with an increasing shrink factor ***)
-sledgehammer_params [shrink_factor = 1]
+sledgehammer_params [isar_proof, isar_shrink_factor = 1]
lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -58,7 +58,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
qed
-sledgehammer_params [shrink_factor = 2]
+sledgehammer_params [isar_proof, isar_shrink_factor = 2]
lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -80,7 +80,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
qed
-sledgehammer_params [shrink_factor = 3]
+sledgehammer_params [isar_proof, isar_shrink_factor = 3]
lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -99,7 +99,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero)
qed
-sledgehammer_params [shrink_factor = 4]
+sledgehammer_params [isar_proof, isar_shrink_factor = 4]
lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -118,7 +118,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
qed
-sledgehammer_params [shrink_factor = 1]
+sledgehammer_params [isar_proof, isar_shrink_factor = 1]
lemma bigo_alt_def: "O(f) =
{h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"