Changes

Summary

1. proper option argument;
2. prefer Isabelle shasum over the old command-line tool with its extra marker character;
3. tuned signature;
4. tuned signature; clarified modules;
5. tuned text, without update of component for now;
6. omit somewhat pointless integrity check;
7. tuned;
8. compile TPTP module
9. compile mirabelle
10. further modernized E setup
11. cleaned up obsolete E setup and a bit of SPASS
12. second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
13. first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
14. updated vscode_extension;
15. added parentheses in TPTP output -- seem necessary for some provers