--- a/src/HOL/TPTP/MaSh_Eval.thy Mon Sep 08 13:56:27 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy Mon Sep 08 13:56:28 2014 +0200
@@ -5,7 +5,7 @@
header {* MaSh Evaluation Driver *}
theory MaSh_Eval
-imports MaSh_Export
+imports MaSh_Export_Base
begin
ML_file "mash_eval.ML"
@@ -23,11 +23,7 @@
*}
ML {*
-val do_it = false (* switch to "true" to generate the files *)
val params = Sledgehammer_Commands.default_params @{theory} []
-val range = (1, NONE)
-val dir = "List"
-val prefix = "/tmp/" ^ dir ^ "/"
val prob_dir = prefix ^ "mash_problems"
*}
--- a/src/HOL/TPTP/MaSh_Export.thy Mon Sep 08 13:56:27 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Mon Sep 08 13:56:28 2014 +0200
@@ -5,40 +5,9 @@
header {* MaSh Exporter *}
theory MaSh_Export
-imports Main
+imports MaSh_Export_Base
begin
-ML_file "mash_export.ML"
-
-sledgehammer_params
- [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
- lam_trans = lifting, timeout = 2, dont_preplay, minimize]
-
-declare [[sledgehammer_fact_duplicates = true]]
-declare [[sledgehammer_instantiate_inducts = false]]
-
-hide_fact (open) HOL.ext
-
-ML {*
-Multithreading.max_threads_value ()
-*}
-
-ML {*
-open MaSh_Export
-*}
-
-ML {*
-val do_it = false (* switch to "true" to generate the files *)
-val thys = [@{theory List}]
-val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
-val prover = hd provers
-val range = (1, NONE)
-val step = 1
-val max_suggestions = 1024
-val dir = "List"
-val prefix = "/tmp/" ^ dir ^ "/"
-*}
-
ML {*
if do_it then
Isabelle_System.mkdir (Path.explode prefix)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy Mon Sep 08 13:56:28 2014 +0200
@@ -0,0 +1,42 @@
+(* Title: HOL/TPTP/MaSh_Export_Base.thy
+ Author: Jasmin Blanchette, TU Muenchen
+*)
+
+header {* MaSh Exporter Base *}
+
+theory MaSh_Export_Base
+imports Main
+begin
+
+ML_file "mash_export.ML"
+
+sledgehammer_params
+ [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
+ lam_trans = lifting, timeout = 2, dont_preplay, minimize]
+
+declare [[sledgehammer_fact_duplicates = true]]
+declare [[sledgehammer_instantiate_inducts = false]]
+
+hide_fact (open) HOL.ext
+
+ML {*
+Multithreading.max_threads_value ()
+*}
+
+ML {*
+open MaSh_Export
+*}
+
+ML {*
+val do_it = false (* switch to "true" to generate the files *)
+val thys = [@{theory List}]
+val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
+val prover = hd provers
+val range = (1, NONE)
+val step = 1
+val max_suggestions = 1024
+val dir = "List"
+val prefix = "/tmp/" ^ dir ^ "/"
+*}
+
+end