equal
deleted
inserted
replaced
334 chain_direct_proof |
334 chain_direct_proof |
335 #> kill_useless_labels_in_proof |
335 #> kill_useless_labels_in_proof |
336 #> relabel_proof |
336 #> relabel_proof |
337 val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) = |
337 val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) = |
338 refute_graph |
338 refute_graph |
|
339 (* |
|
340 |> tap (tracing o prefix "REFUTE: " o string_of_refute_graph) |
|
341 *) |
339 |> redirect_graph axioms tainted bot |
342 |> redirect_graph axioms tainted bot |
|
343 (* |
|
344 |> tap (tracing o prefix "DIRECT: " o string_of_direct_proof) |
|
345 *) |
340 |> isar_proof_of_direct_proof |
346 |> isar_proof_of_direct_proof |
341 |> relabel_proof_canonically |
347 |> relabel_proof_canonically |
342 |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay |
348 |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay |
343 preplay_timeout) |
349 preplay_timeout) |
344 val ((preplay_time, preplay_fail), isar_proof) = |
350 val ((preplay_time, preplay_fail), isar_proof) = |