Changes

Summary

1. compile
2. updated Sledgehammer documentation
3. a more generous hard timeout
4. early warning when Sledgehammer finds a proof
5. another 'corec' example
6. don't ask too much of 'transfer_prover'
7. commented out for now
8. tuning
9. FIXME
10. avoid 'prove_sorry' for unreliable tactics
11. reused code
12. tuning
13. tuned examples
14. new 'corec' example
15. more reliable check for rhs variables
16. strengthened tactic
17. generalized ML function
18. added '_legacy' suffixes
19. generalized ML interface
20. tuning
21. refined experimental option of Sledgehammer