Changes

Summary

1. more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
2. enable induction in one of Zipperposition's slices
3. made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme
4. robustly handle empty proof blocks in Isar proof output
5. propagate right result when enough proofs have been found
6. correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives
7. don't lose error messages
8. don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
9. careful with partial applications
10. don't perform preplaying steps if preplaying is disabled
11. adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
12. tuned punctuation
13. handle TPTP '!=' more gracefully in Isar proof reconstruction
14. guard against duplicate lines in Zipperposition proofs