equal
deleted
inserted
replaced
321 |> postprocess_isar_proof_remove_unreferenced_steps |
321 |> postprocess_isar_proof_remove_unreferenced_steps |
322 (keep_fastest_method_of_isar_step (!preplay_data) |
322 (keep_fastest_method_of_isar_step (!preplay_data) |
323 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |
323 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |
324 |> tap (trace_isar_proof "Minimized") |
324 |> tap (trace_isar_proof "Minimized") |
325 |> `(preplay_outcome_of_isar_proof (!preplay_data)) |
325 |> `(preplay_outcome_of_isar_proof (!preplay_data)) |
326 ||> comment_isar_proof comment_of |
326 ||> (comment_isar_proof comment_of |
327 ||> chain_isar_proof |
327 #> chain_isar_proof |
328 ||> kill_useless_labels_in_isar_proof |
328 #> kill_useless_labels_in_isar_proof |
329 ||> relabel_isar_proof_nicely |
329 #> relabel_isar_proof_nicely) |
330 in |
330 in |
331 (case string_of_isar_proof isar_proof of |
331 (case string_of_isar_proof isar_proof of |
332 "" => |
332 "" => |
333 if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)." |
333 if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)." |
334 else "" |
334 else "" |