equal
deleted
inserted
replaced
360 let |
360 let |
361 val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) |
361 val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) |
362 val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof |
362 val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof |
363 val preferred_methss = |
363 val preferred_methss = |
364 (Metis_Method (NONE, NONE), |
364 (Metis_Method (NONE, NONE), |
365 bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types |
365 bunches_of_proof_methods try0 smt_proofs needs_full_types |
366 (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) |
366 (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) |
367 in |
367 in |
368 (used_facts, preferred_methss, |
368 (used_facts, preferred_methss, |
369 fn preplay => |
369 fn preplay => |
370 let |
370 let |
371 val _ = if verbose then writeln "Generating proof text..." else () |
371 val _ = if verbose then writeln "Generating proof text..." else () |