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.

Basic support for the SMT prover veriT.

removing the '= True' generated by Leo-II.

Skolemization support for leo-II and Zipperposition.

document property 'set_induct'

generate 'set_induct' theorem for codatatypes

also try 'metis' with 'full_types'

header tuning

correctly translate THF functions from terms to types