--- a/src/HOL/TPTP/MaSh_Import.thy Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy Tue Jul 10 23:36:03 2012 +0200
@@ -9,6 +9,10 @@
uses "mash_import.ML"
begin
+sledgehammer_params
+ [max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
+ lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
+
declare [[sledgehammer_instantiate_inducts]]
ML {*
@@ -16,12 +20,12 @@
*}
ML {*
-val do_it = true (* switch to "true" to generate the files *);
-val thy = @{theory List}
+val do_it = false (* switch to "true" to generate the files *);
+val thy = @{theory Nat}
*}
ML {*
-if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions2"
+if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions"
else ()
*}