Giving the "--silent" switch to E, to produce less output
authorpaulson
Mon May 29 16:18:31 2006 +0200 (2006-05-29 ago)
changeset 1974473aab222fecb
parent 19743 0843210d3756
child 19745 df6fd56d63a9
Giving the "--silent" switch to E, to produce less output
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon May 29 13:15:53 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon May 29 16:18:31 2006 +0200
     1.3 @@ -388,7 +388,7 @@
     1.4  	       let val Eprover = helper_path "E_HOME" "eproof"
     1.5  	       in
     1.6  		  ("E", Eprover, 
     1.7 -		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time, probfile) ::
     1.8 +		     "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) ::
     1.9  		   make_atp_list xs (n+1)
    1.10  	       end
    1.11  	     else error ("Invalid prover name: " ^ !prover)