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

do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly

back to post-release mode -- after fork point;

tuned;

tuned;

no -optimise -- produces bad bytecode;

output state first -- avoid fluctuation wrt. warnings, errors, etc.;

tuned comment;

updated to polyml-5.5.2-1 which addresses two hard crashes;

updated to cygwin-20140725, which is presumably close to Cygwin 1.7.31-1;