# 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 \ Z) = @@ -133,7 +133,7 @@ by (metis 18 17) qed -declare [[sledgehammer_modulus = 3]] +sledgehammer_params [modulus = 3] lemma (*equal_union: *) "(X = Y \ Z) = @@ -168,7 +168,7 @@ (*Example included in TPHOLs paper*) -declare [[sledgehammer_modulus = 4]] +sledgehammer_params [modulus = 4] lemma (*equal_union: *) "(X = Y \ Z) =