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

imported patch hilbert_choice_support

veriT changes for lifted terms, and ite_elim rules.

imported patch satallax_proof_support_Sledgehammer

Basic support for the higher-order ATP Satallax.

Subproofs for the SMT solver veriT.