some cleanup in Function_Lib

merged

compile

added SMT solver to Sledgehammer docs

more robust handling of "remote_" vs. non-"remote_" provers

generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)

replaced references with proper record that's threaded through

fixed signature of "is_smt_solver_installed"; renaming

renamed modules

renamed files

took out "smt"/"remote_smt" from default ATPs until they are properly implemented

remove more needless code ("run_smt_solvers"); tuning

got rid of duplicate functionality ("run_smt_solver_somehow"); added minimization command to SMT solver message

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