src/HOL/Tools/ATP/atp_systems.ML

 
 
 (* SPASS *)
 
 (* The "-VarWeight=3" option helps the higher-order problems, probably by
-   counteracting the presence of "hAPP". *)
+   counteracting the presence of explicit application operators. *)
 val spass_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \