leverage new data structure for handling "add:" and "del:"

thread original theorem along with CNF theorem, as a step toward killing the Skolem cache

merge "generic_prover" and "generic_tptp_prover"

removed Sledgehammer's support for the DFG syntax; this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.

distinguish between "unknown" and "no Kodkodi installed" errors

reintroduce new Sledgehammer polymorphic handling code; this time I tested the proper version of Isabelle

make the Nitpick_Example theory processable even when Kodkodi is not installed; so that at least the "theory" aspects of it (as opposed to the diagnosis offered by Nitpick) are checked on everybody's machines

Make latex happy

Quotient package now uses Partial Equivalence instead place of equivalence

Replace 'list_rel' by 'list_all2'; they are equivalent.

Proper treatment of non-inherited mixins.

merged

Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.

reredisable new polymorphic code

merged

beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later; reintroduced old proof based on Metis, since it was a good test for the Skolemizer