equal
deleted
inserted
replaced
11 fun done _ _ = () |
11 fun done _ _ = () |
12 |
12 |
13 fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) = |
13 fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) = |
14 let |
14 let |
15 val thms = Mirabelle.theorems_of_sucessful_proof post |
15 val thms = Mirabelle.theorems_of_sucessful_proof post |
16 val names = map Thm.get_name thms |
16 val names = map Thm.get_name_hint thms |
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 (ProofContext.facts_of (Proof.context_of pre)) |
19 val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre)) |
20 |
20 |
21 fun metis ctxt = Metis_Tactics.metis_tac ctxt (thms @ facts) |
21 fun metis ctxt = Metis_Tactics.metis_tac ctxt (thms @ facts) |