equal
deleted
inserted
replaced
14 val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre)) |
14 val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre)) |
15 |
15 |
16 fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts) |
16 fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts) |
17 in |
17 in |
18 (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |
18 (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |
|
19 |> prefix "metis: " |
19 |> add_info |
20 |> add_info |
20 |> log |
21 |> log |
21 end |
22 end |
|
23 handle TimeLimit.TimeOut => log "metis: time out" |
22 |
24 |
23 fun invoke _ = Mirabelle.register ("metis", metis_action) |
25 fun invoke _ = Mirabelle.register ("metis", metis_action) |
24 |
26 |
25 end |
27 end |