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

added more proof methods for one-liners

unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)

Improving robustness and indentation corrections.

Skolemization for tmp_ite_elim rule in the SMT solver veriT.

Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.

Whitespace and indentation correction.

Simplifying the labels in the proof of the SMT solver veriT.

Changing ~ into - for unuary minus (not supported by veriT)

imported patch satallax_skolemization_in_tree_part