author | blanchet |
Tue, 04 Feb 2014 23:11:18 +0100 | |
changeset 55324 | e04b75bd18e0 |
parent 55323 | 253a029335a2 |
child 55325 | 462ffd3b7065 |
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML | file | annotate | diff | comparison | revisions |
--- 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)) =