23 |
23 |
24 open Sledgehammer_Proof_Methods |
24 open Sledgehammer_Proof_Methods |
25 open Sledgehammer_Isar_Proof |
25 open Sledgehammer_Isar_Proof |
26 open Sledgehammer_Isar_Preplay |
26 open Sledgehammer_Isar_Preplay |
27 |
27 |
28 fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, _)) = |
28 fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, meths)) = |
29 Prove (qs, xs, l, t, subproofs, facts, [fastest_method_of_isar_step preplay_data l]) |
29 Prove (qs, xs, l, t, subproofs, facts, |
|
30 meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @) |
30 | keep_fastest_method_of_isar_step _ step = step |
31 | keep_fastest_method_of_isar_step _ step = step |
31 |
32 |
32 val slack = seconds 0.1 |
33 val slack = seconds 0.1 |
33 |
34 |
34 fun minimize_isar_step_dependencies ctxt preplay_data |
35 fun minimize_isar_step_dependencies ctxt preplay_data |