--- a/src/HOL/ROOT Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/ROOT Sun Jun 29 18:30:24 2014 +0200
@@ -665,7 +665,6 @@
theories
ATP_Theory_Export
MaSh_Eval
- MaSh_Export
TPTP_Interpret
THF_Arith
TPTP_Proof_Reconstruction
--- a/src/HOL/TPTP/MaSh_Eval.thy Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy Sun Jun 29 18:30:24 2014 +0200
@@ -5,7 +5,7 @@
header {* MaSh Evaluation Driver *}
theory MaSh_Eval
-imports Complex_Main
+imports MaSh_Export
begin
ML_file "mash_eval.ML"
--- a/src/HOL/TPTP/mash_eval.ML Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Sun Jun 29 18:30:24 2014 +0200
@@ -125,13 +125,12 @@
in
Config.put atp_dest_dir dir
#> Config.put atp_problem_prefix (prob_prefix ^ "__")
- #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
+ #> Config.put SMT2_Config.debug_files (dir ^ "/" ^ prob_prefix)
end
| set_file_name _ NONE = I
fun prove method suggs =
- if not (member (op =) methods method) orelse
- (null facts andalso method <> IsarN) then
+ if not (member (op =) methods method) orelse (null facts andalso method <> IsarN) then
(str_of_method method ^ "Skipped", 0)
else
let
@@ -146,8 +145,7 @@
|> take (the max_facts)
|> map fact_of_raw_fact
val ctxt = ctxt |> set_file_name method prob_dir_name
- val res as {outcome, ...} =
- run_prover_for_mash ctxt params prover name facts goal
+ val res as {outcome, ...} = run_prover_for_mash ctxt params prover name facts goal
val ok = if is_none outcome then 1 else 0
in
(str_of_result method facts res, ok)
@@ -170,9 +168,8 @@
zeros
fun total_of method ok n =
- str_of_method method ^ string_of_int ok ^ " (" ^
- Real.fmt (StringCvt.FIX (SOME 1))
- (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
+ str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1))
+ (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
val inst_inducts = Config.get ctxt instantiate_inducts
val options =