tuned slack
authorblanchet
Tue, 04 Feb 2014 23:11:18 +0100
changeset 55324 e04b75bd18e0
parent 55323 253a029335a2
child 55325 462ffd3b7065
tuned slack
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Tue Feb 04 23:11:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -32,7 +32,7 @@
       comment)
   | keep_fastest_method_of_isar_step _ step = step
 
-val slack = seconds 0.1
+val slack = seconds 0.025
 
 fun minimize_isar_step_dependencies ctxt preplay_data
       (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =