restored a bit of laziness

reorder quantifiers to ease Z3 skolemization

tuned order of arguments

tuned name context code

tuned whitespace

more rational unskolemizing of names

added appropriate method for skolemization of Z3 steps to the mix

pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)

honor 'try0' also for one-liners

tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence

further minimize one-liner

tuning

eliminated needlessly complex message tail

updated NEWS

update documentation after removal of 'min' subcommand

eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)

rationalized preplaying by eliminating (now superfluous) laziness

removed proof methods as provers from docs

simplified minimization logic

tuning

remove lambda-lifting related assumptions from generated Isar proofs

whitespace tuning

remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer

generate backquotes without markup, since this confuses preplay; bump up spying version identifier;

simplified tactics slightly

cascading timeout in parallel evaluation, to rapidly find optimum

put faster proof methods first

use parallel preplay machinery also for one-line proofs

updated docs

always minimize Sledgehammer results by default

tuned ML function name

reduced preplay timeout to 1 s