add dependency of "spass" script
authorblanchet
Wed, 01 Sep 2010 22:31:45 +0200
changeset 39002 a2d7be688ea1
parent 39001 42e6eb597c30
child 39003 c2aebd79981f
add dependency of "spass" script
src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 01 21:47:25 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 01 22:31:45 2010 +0200
@@ -168,7 +168,7 @@
    counteracting the presence of "hAPP". *)
 val spass_config : prover_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
-   required_execs = [("SPASS_HOME", "SPASS")],
+   required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
    arguments = fn complete => fn timeout =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))