--- a/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200
@@ -9,10 +9,6 @@
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 {*
@@ -20,13 +16,15 @@
*}
ML {*
-val do_it = false (* switch to "true" to generate the files *);
+val do_it = true (* switch to "true" to generate the files *);
val thy = @{theory List}
*}
ML {*
-if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
-else ()
+if do_it then
+ import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
+else
+ ()
*}
end