equal
deleted
inserted
replaced
432 |
432 |
433 val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal |
433 val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal |
434 |
434 |
435 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = |
435 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = |
436 let |
436 let |
437 open Metis_Clauses |
437 open Metis_Translate |
438 val thy = Proof.theory_of st |
438 val thy = Proof.theory_of st |
439 val n0 = length (these (!named_thms)) |
439 val n0 = length (these (!named_thms)) |
440 val (prover_name, _) = get_atp thy args |
440 val (prover_name, _) = get_atp thy args |
441 val timeout = |
441 val timeout = |
442 AList.lookup (op =) args minimize_timeoutK |
442 AList.lookup (op =) args minimize_timeoutK |