src/HOL/Metis_Examples/Big_O.thy
changeset 51130 76d68444cd59
parent 50020 6b9611abcd4c
child 53015 a1119cf551e8
--- a/src/HOL/Metis_Examples/Big_O.thy	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Feb 14 22:49:22 2013 +0100
@@ -29,7 +29,7 @@
 
 (*** Now various verions with an increasing shrink factor ***)
 
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -60,7 +60,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 2]
+sledgehammer_params [isar_proofs, isar_compress = 2]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -83,7 +83,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 3]
+sledgehammer_params [isar_proofs, isar_compress = 3]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -103,7 +103,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 4]
+sledgehammer_params [isar_proofs, isar_compress = 4]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -123,7 +123,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
 
 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
 by (auto simp add: bigo_def bigo_pos_const)