escape backticks in altstrings

added a timestamp to Nitpick in verbose mode for debugging purposes; turn on verbose mode for the examples

reduce the minimizer slack and add verbose information

two layers of timeouts seem to be less reliable than a single layer

move relevance filter into hard timeout

handle timeouts in Mirabelle more gracefully

made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever); disabled inductions (E and SPASS don't like them), but kept "ext" (seems more harmless)

Add mixins to locale dependencies.

Enable show_hyps, which appears to be set in batch mode but in an interactive session.

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;

remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)

more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle

convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented

merged

put the SMT weights back where they belong, so that they're also used by Mirabelle

added debugging option to find out how good the relevance filter was at identifying relevant facts

extra checking of name bindings for classes, types, consts; tuned;

more explicit references to structure Raw_Simplifier;

merged

merged

merged