# HG changeset patch # User blanchet # Date 1328444931 -3600 # Node ID 4a2deac585f8b7fcf9b68936252d330638702893 # Parent b040e50f17fd2ddfdb1c7064f8bab1cd82a75a9a remove option that's on by default diff -r b040e50f17fd -r 4a2deac585f8 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun Feb 05 12:27:10 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Feb 05 13:28:51 2012 +0100 @@ -360,7 +360,7 @@ required_execs = [], arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ => (* TODO: add: -FPDFGProof -FPFCR *) - ("-Auto -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) + ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) (* TODO: not used yet *) |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ", proof_delims = #proof_delims spass_config,