equal
deleted
inserted
replaced
305 () |
305 () |
306 |
306 |
307 val (play_outcome, isar_proof) = |
307 val (play_outcome, isar_proof) = |
308 canonical_isar_proof |
308 canonical_isar_proof |
309 |> tap (trace_isar_proof "Original") |
309 |> tap (trace_isar_proof "Original") |
310 |> compress_isar_proof compress_isar preplay_data |
310 |> compress_isar_proof preplay_ctxt compress_isar preplay_data |
311 |> tap (trace_isar_proof "Compressed") |
311 |> tap (trace_isar_proof "Compressed") |
312 |> try0_isar ? try0_isar_proof preplay_timeout preplay_data |
312 |> try0_isar ? try0_isar_proof preplay_ctxt preplay_timeout preplay_data |
313 |> tap (trace_isar_proof "Tried0") |
313 |> tap (trace_isar_proof "Tried0") |
314 |> postprocess_isar_proof_remove_unreferenced_steps |
314 |> postprocess_isar_proof_remove_unreferenced_steps |
315 (try0_isar ? minimize_isar_step_dependencies preplay_data) |
315 (try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data) |
316 |> tap (trace_isar_proof "Minimized") |
316 |> tap (trace_isar_proof "Minimized") |
317 |> `overall_preplay_outcome |
317 |> `overall_preplay_outcome |
318 ||> chain_isar_proof |
318 ||> chain_isar_proof |
319 ||> kill_useless_labels_in_isar_proof |
319 ||> kill_useless_labels_in_isar_proof |
320 ||> relabel_isar_proof_finally |
320 ||> relabel_isar_proof_finally |