# HG changeset patch
# User blanchet
# Date 1358424704 -3600
# Node ID dfc0177384f94f9ec7481227a19fc81e14500c09
# Parent  beb95bf66b21f4fa800eb07b41753699fcc7ce6e
tweaked defaults

diff -r beb95bf66b21 -r dfc0177384f9 src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Thu Jan 17 11:56:34 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Thu Jan 17 13:11:44 2013 +0100
@@ -12,9 +12,9 @@
 
 sledgehammer_params
   [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
-   lam_trans = combs_and_lifting, timeout = 15, dont_preplay, minimize]
+   lam_trans = lifting, timeout = 15, dont_preplay, minimize]
 
-declare [[sledgehammer_instantiate_inducts]]
+declare [[sledgehammer_instantiate_inducts = false]]
 
 ML {*
 !Multithreading.max_threads
diff -r beb95bf66b21 -r dfc0177384f9 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 11:56:34 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 13:11:44 2013 +0100
@@ -12,9 +12,9 @@
 
 sledgehammer_params
   [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
-   lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize]
+   lam_trans = lifting, timeout = 2, dont_preplay, minimize]
 
-declare [[sledgehammer_instantiate_inducts]]
+declare [[sledgehammer_instantiate_inducts = false]]
 
 ML {*
 !Multithreading.max_threads
@@ -29,7 +29,7 @@
 val thys = [@{theory List}]
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
-val max_suggestions = 1024
+val max_suggestions = 1536
 val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
 *}