# HG changeset patch # User huffman # Date 1235051426 28800 # Node ID bdf83fc2c8ba97a8122f39abea84710622b59ea0 # Parent 747f0c519090f85284bf3753778a5025af87485c# Parent 015c56cc186498649c0020ec08509c64fef1474a merged diff -r 747f0c519090 -r bdf83fc2c8ba src/Tools/auto_solve.ML --- a/src/Tools/auto_solve.ML Wed Feb 18 20:53:58 2009 -0800 +++ b/src/Tools/auto_solve.ML Thu Feb 19 05:50:26 2009 -0800 @@ -23,7 +23,7 @@ structure FT = FindTheorems; val auto = ref false; - val auto_time_limit = ref 5000; + val auto_time_limit = ref 2500; fun seek_solution int state = let val ctxt = Proof.context_of state;