crude implementation of centralized slicing

removed obscure E option

take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set

rationalize slicing format

thread slices through

simplified 'best_slice' data structure and made minor changes to slices

changed logic of 'slice' option to 'slices'

updated documentation of 'slice' (now 'slices') option

revised Sledgehammer documentation

rationalized output for forthcoming slicing model

use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code

disable slicing within ATP module (in preparation for refactoring)

disable slicing within SMT (in preparation for factoring it out)

generalized the 'slice' option towards more flexible slicing

tuned -- fewer warnings;

Added a tiny proof

Deletion of a duplicate proof

useful lemma integral_less

merged

removed unused parameter following f9908452b282

treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)

fixed dodgy intro! attributes

merged

optimized facts traversal in TPTP translation

optimized app_op_level selection in TPTP generation

tuned trivial check in mirabelle_sledgehammer

renamed run_action to run in Mirabelle.action record

added spying of fact filtering timing

tuned mirabelle_sledgehammer output

added spying to Sledgehammer

proper fact filter for dummy ATPs

added syping of fact filtering time to sledgehammer