compile

use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)

repaired theory merging and defined/used helpers

make Sledgehammer a little bit less verbose in "try"

handle non-auto try cases gracefully in Try Methods

handle non-auto try case gracefully in Solve Direct

prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators

update SML section of documentation

handle non-auto try case gracefully in Nitpick

handle non-auto try case of Sledgehammer better

added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods

removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments

renamed "Auto_Tools" "Try"

removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP

renamed "try" "try_methods"

renamed "metis_timeout" to "preplay_timeout" and continued implementation

minor fixes to Sledgehammer docs

shorten minimizer command further, exploiting until-now-undocumented syntax

minor tweaks to the Nitpick documentation

added syntax for specifying Metis timeout (currently used only by SMT solvers)

readded Waldmeister as default to the documentation and other minor changes

reintroduced Waldmeister but limit the number of remote threads created

renamed "minimize" to "min" to make Sledgehammer output a little bit more concise

minor doc adjustments

make output more concise

merge timeout messages from several ATPs into one message to avoid clutter

fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context

tuning

mention contributions from LCP and explain metis and metisFT encodings

fixed trivial fact detection