# HG changeset patch
# User blanchet
# Date 1273869024 -7200
# Node ID ffad77bb3046e82b3501ddd3ea68adab2b76db90
# Parent  ff01d3ae9ad451e4cdcc691e9507f7745ace4198
renamed Sledgehammer options

diff -r ff01d3ae9ad4 -r ffad77bb3046 src/HOL/Metis_Examples/BigO.thy
--- 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)))}"
diff -r ff01d3ae9ad4 -r ffad77bb3046 src/HOL/Metis_Examples/TransClosure.thy
--- a/src/HOL/Metis_Examples/TransClosure.thy	Fri May 14 22:29:50 2010 +0200
+++ b/src/HOL/Metis_Examples/TransClosure.thy	Fri May 14 22:30:24 2010 +0200
@@ -39,7 +39,7 @@
 
 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proof, shrink_factor = 2] *)
+(* sledgehammer [isar_proof, isar_shrink_factor = 2] *)
 proof -
   assume A1: "f c = Intg x"
   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
diff -r ff01d3ae9ad4 -r ffad77bb3046 src/HOL/Metis_Examples/set.thy
--- a/src/HOL/Metis_Examples/set.thy	Fri May 14 22:29:50 2010 +0200
+++ b/src/HOL/Metis_Examples/set.thy	Fri May 14 22:30:24 2010 +0200
@@ -16,7 +16,7 @@
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
-sledgehammer_params [shrink_factor = 1]
+sledgehammer_params [isar_proof, isar_shrink_factor = 1]
 
 (*multiple versions of this example*)
 lemma (*equal_union: *)
@@ -85,7 +85,7 @@
   by (metis 31 29)
 qed
 
-sledgehammer_params [shrink_factor = 2]
+sledgehammer_params [isar_proof, isar_shrink_factor = 2]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =
@@ -128,7 +128,7 @@
   by (metis 18 17)
 qed
 
-sledgehammer_params [shrink_factor = 3]
+sledgehammer_params [isar_proof, isar_shrink_factor = 3]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =
@@ -163,7 +163,7 @@
 
 (*Example included in TPHOLs paper*)
 
-sledgehammer_params [shrink_factor = 4]
+sledgehammer_params [isar_proof, isar_shrink_factor = 4]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =