src/HOL/Metis_Examples/Big_O.thy
changeset 49918 cf441f4a358b
parent 47445 69e96e5500df
child 50020 6b9611abcd4c
     1.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Thu Oct 18 14:26:45 2012 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Oct 18 15:05:17 2012 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  (*** Now various verions with an increasing shrink factor ***)
     1.6  
     1.7 -sledgehammer_params [isar_proof, isar_shrink_factor = 1]
     1.8 +sledgehammer_params [isar_proofs, isar_shrinkage = 1]
     1.9  
    1.10  lemma
    1.11    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    1.12 @@ -60,7 +60,7 @@
    1.13    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
    1.14  qed
    1.15  
    1.16 -sledgehammer_params [isar_proof, isar_shrink_factor = 2]
    1.17 +sledgehammer_params [isar_proofs, isar_shrinkage = 2]
    1.18  
    1.19  lemma
    1.20    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    1.21 @@ -83,7 +83,7 @@
    1.22    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
    1.23  qed
    1.24  
    1.25 -sledgehammer_params [isar_proof, isar_shrink_factor = 3]
    1.26 +sledgehammer_params [isar_proofs, isar_shrinkage = 3]
    1.27  
    1.28  lemma
    1.29    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    1.30 @@ -103,7 +103,7 @@
    1.31    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
    1.32  qed
    1.33  
    1.34 -sledgehammer_params [isar_proof, isar_shrink_factor = 4]
    1.35 +sledgehammer_params [isar_proofs, isar_shrinkage = 4]
    1.36  
    1.37  lemma
    1.38    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    1.39 @@ -123,7 +123,7 @@
    1.40    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
    1.41  qed
    1.42  
    1.43 -sledgehammer_params [isar_proof, isar_shrink_factor = 1]
    1.44 +sledgehammer_params [isar_proofs, isar_shrinkage = 1]
    1.45  
    1.46  lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
    1.47  by (auto simp add: bigo_def bigo_pos_const)