# HG changeset patch
# User blanchet
# Date 1270112061 -7200
# Node ID 3a074096f83aca53d18898a8d8dedbac9e118fc0
# Parent  1493b43204e92bb51bf336ee6f22e372b7a0a95e
adapt syntax of Sledgehammer options in examples

diff -r 1493b43204e9 -r 3a074096f83a src/HOL/Metis_Examples/BigO.thy
--- a/src/HOL/Metis_Examples/BigO.thy	Thu Apr 01 10:27:06 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy	Thu Apr 01 10:54:21 2010 +0200
@@ -28,7 +28,7 @@
 
 (*** Now various verions with an increasing modulus ***)
 
-declare [[sledgehammer_modulus = 1]]
+sledgehammer_params [modulus = 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
 
-declare [[sledgehammer_modulus = 2]]
+sledgehammer_params [modulus = 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
 
-declare [[sledgehammer_modulus = 3]]
+sledgehammer_params [modulus = 3]
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -170,7 +170,7 @@
 qed
 
 
-declare [[sledgehammer_modulus = 1]]
+sledgehammer_params [modulus = 4]
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -206,7 +206,7 @@
 qed
 
 
-declare [[sledgehammer_sorts = true]]
+sledgehammer_params [sorts]
 
 lemma bigo_alt_def: "O(f) = 
     {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
diff -r 1493b43204e9 -r 3a074096f83a src/HOL/Metis_Examples/set.thy
--- a/src/HOL/Metis_Examples/set.thy	Thu Apr 01 10:27:06 2010 +0200
+++ b/src/HOL/Metis_Examples/set.thy	Thu Apr 01 10:54:21 2010 +0200
@@ -19,7 +19,7 @@
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
-declare [[sledgehammer_modulus = 1]]
+sledgehammer_params [modulus = 1]
 
 
 (*multiple versions of this example*)
@@ -90,7 +90,7 @@
   by (metis 31 29)
 qed
 
-declare [[sledgehammer_modulus = 2]]
+sledgehammer_params [modulus = 2]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =
@@ -133,7 +133,7 @@
   by (metis 18 17)
 qed
 
-declare [[sledgehammer_modulus = 3]]
+sledgehammer_params [modulus = 3]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =
@@ -168,7 +168,7 @@
 
 (*Example included in TPHOLs paper*)
 
-declare [[sledgehammer_modulus = 4]]
+sledgehammer_params [modulus = 4]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =