equal
deleted
inserted
replaced
340 isar_steps outer (SOME l) (step :: accum) infs |
340 isar_steps outer (SOME l) (step :: accum) infs |
341 end |
341 end |
342 and isar_proof outer fix assms lems infs = |
342 and isar_proof outer fix assms lems infs = |
343 Proof (fix, assms, lems @ isar_steps outer NONE [] infs) |
343 Proof (fix, assms, lems @ isar_steps outer NONE [] infs) |
344 |
344 |
345 val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) = |
345 val (preplay_interface as {overall_preplay_outcome, ...}, isar_proof) = |
346 refute_graph |
346 refute_graph |
347 (* |
347 (* |
348 |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph) |
348 |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph) |
349 *) |
349 *) |
350 |> redirect_graph axioms tainted bot |
350 |> redirect_graph axioms tainted bot |
361 isar_proof |
361 isar_proof |
362 |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0) |
362 |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0) |
363 preplay_interface |
363 preplay_interface |
364 |> isar_try0 ? try0 preplay_timeout preplay_interface |
364 |> isar_try0 ? try0 preplay_timeout preplay_interface |
365 |> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface) |
365 |> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface) |
366 |> `overall_preplay_stats |
366 |> `overall_preplay_outcome |
367 ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof) |
367 ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof) |
368 |
368 |
369 val isar_text = |
369 val isar_text = |
370 string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof |
370 string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof |
371 in |
371 in |