--- a/src/HOL/TPTP/MaSh_Import.thy Tue Jul 17 23:11:27 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 18 08:44:03 2012 +0200
@@ -9,6 +9,10 @@
uses "mash_import.ML"
begin
+sledgehammer_params
+ [provers = e, 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 {*
--- a/src/HOL/TPTP/ROOT.ML Tue Jul 17 23:11:27 2012 +0200
+++ b/src/HOL/TPTP/ROOT.ML Wed Jul 18 08:44:03 2012 +0200
@@ -7,6 +7,8 @@
*)
use_thys [
+ "ATP_Theory_Export",
+ "MaSh_Export",
"MaSh_Import",
"TPTP_Interpret",
"THF_Arith"
--- a/src/HOL/TPTP/mash_import.ML Tue Jul 17 23:11:27 2012 +0200
+++ b/src/HOL/TPTP/mash_import.ML Wed Jul 18 08:44:03 2012 +0200
@@ -18,7 +18,6 @@
struct
open Sledgehammer_Filter_MaSh
-open MaSh_Export
val unescape_meta =
let