compile mirabelle

tweaked Auto Sledgehammer's behavior and output

updated NEWS

removed experimental prover z3_tptp

print more verbose information

run all installed provers by default

update slice options centrally

further work on new Sledgehammer slicing

tweaked verbose output

tweak padding of prover slice schedule to include all provers

implemented 'max_proofs' mechanism

document new option 'max_proofs'

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