bring ATPs and SMT solvers more in line with each other

make Sledgehammer minimizer fully work with SMT

generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well

first step in adding support for an SMT backend to Sledgehammer

use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."

cosmetics

relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version

Changed section title to please LaTeX.

temporary removed Predicate_Compile_Quickcheck_Examples from tests

adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog

using a signature in core_data and moving some more functions to core_data

splitting large core file into core_data, mode_inference and predicate_compile_proof

added generator_dseq compilation for a sound depth-limited compilation with small value generators

for now safely but unpractically assume no predicate is terminating

adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible