Add mixins to sublocale command.

tuning

higher hard timeout

lower threshold where the binary algorithm kick in and use the same value for automatic minimization

compile

let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)

use minimizing prover in Mirabelle

renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"

factored out running a prover with (optionally) an implicit minimizer phrase

merged;