# HG changeset patch # User paulson # Date 1148912311 -7200 # Node ID 73aab222fecbd231399d1a16d4fe7659559e26a8 # Parent 0843210d3756863267edc15caaabda490c512ce4 Giving the "--silent" switch to E, to produce less output diff -r 0843210d3756 -r 73aab222fecb src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Mon May 29 13:15:53 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Mon May 29 16:18:31 2006 +0200 @@ -388,7 +388,7 @@ let val Eprover = helper_path "E_HOME" "eproof" in ("E", Eprover, - "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time, probfile) :: + "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) :: make_atp_list xs (n+1) end else error ("Invalid prover name: " ^ !prover)