--- 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)