add type annotation to avoid warning

simplify some proofs, convert to Isar style

rename lemma spair_lemma to spair_Sprod

pcpodef (open) 'a lift

remove intro! attribute from {sinl,sinr}_defined

simplify proofs of ssumE, sprodE

merged

renamed nat_number

nat_number -> eval_nat_numeral

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.