equal
deleted
inserted
replaced
17 val add_info = if null names then I else suffix (":\n" ^ commas names) |
17 val add_info = if null names then I else suffix (":\n" ^ commas names) |
18 |
18 |
19 val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) |
19 val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) |
20 |
20 |
21 fun metis ctxt = |
21 fun metis ctxt = |
22 Metis_Tactic.metis_tac [] ATP_Translate.lam_liftingN ctxt (thms @ facts) |
22 Metis_Tactic.metis_tac [] ATP_Problem_Generate.lam_liftingN ctxt |
|
23 (thms @ facts) |
23 in |
24 in |
24 (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |
25 (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |
25 |> prefix (metis_tag id) |
26 |> prefix (metis_tag id) |
26 |> add_info |
27 |> add_info |
27 |> log |
28 |> log |