src/HOL/MetisExamples/set.thy

--- a/src/HOL/MetisExamples/set.thy	Wed Mar 19 14:25:59 2008 +0100
+++ b/src/HOL/MetisExamples/set.thy	Wed Mar 19 18:10:23 2008 +0100
@@ -20,7 +20,8 @@
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
-declare [[reconstruction_modulus = 1]]
+declare [[sledgehammer_full = true]]
+declare [[sledgehammer_modulus = 1]]
 
 (*multiple versions of this example*)
 lemma (*equal_union: *)
@@ -90,7 +91,7 @@
   by (metis 31 29)
 qed
 
-declare [[reconstruction_modulus = 2]]
+declare [[sledgehammer_modulus = 2]]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =
@@ -133,7 +134,7 @@
   by (metis 18 17)
 qed
 
-declare [[reconstruction_modulus = 3]]
+declare [[sledgehammer_modulus = 3]]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =
@@ -168,7 +169,7 @@
 
 (*Example included in TPHOLs paper*)
 
-declare [[reconstruction_modulus = 4]]
+declare [[sledgehammer_modulus = 4]]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =