src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
changeset 55324 e04b75bd18e0
parent 55314 e0233567a8ef
child 55452 29ec8680e61f
--- 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)) =