30 Prove (qs, xs, l, t, subproofs, facts, |
30 Prove (qs, xs, l, t, subproofs, facts, |
31 meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @, |
31 meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @, |
32 comment) |
32 comment) |
33 | keep_fastest_method_of_isar_step _ step = step |
33 | keep_fastest_method_of_isar_step _ step = step |
34 |
34 |
35 val slack = seconds 0.1 |
35 val slack = seconds 0.025 |
36 |
36 |
37 fun minimize_isar_step_dependencies ctxt preplay_data |
37 fun minimize_isar_step_dependencies ctxt preplay_data |
38 (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) = |
38 (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) = |
39 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
39 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
40 Played time => |
40 Played time => |