Changes

Summary

1. tuning
2. tuned NEWS
3. compile HOL-TPTP
4. compile Metis_Examples
5. more NEWS
6. compile mirabelle
7. tweaked Auto Sledgehammer's behavior and output
8. updated NEWS
9. removed experimental prover z3_tptp
10. print more verbose information
11. run all installed provers by default
12. update slice options centrally
13. further work on new Sledgehammer slicing
14. tweaked verbose output
15. tweak padding of prover slice schedule to include all provers
16. implemented 'max_proofs' mechanism
17. document new option 'max_proofs'
18. crude implementation of centralized slicing
19. removed obscure E option
20. take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
21. rationalize slicing format
22. thread slices through
23. simplified 'best_slice' data structure and made minor changes to slices
24. changed logic of 'slice' option to 'slices'
25. updated documentation of 'slice' (now 'slices') option
26. revised Sledgehammer documentation
27. rationalized output for forthcoming slicing model
28. use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
29. disable slicing within ATP module (in preparation for refactoring)
30. disable slicing within SMT (in preparation for factoring it out)
31. generalized the 'slice' option towards more flexible slicing