Summary
- compile
- updated Sledgehammer documentation
- a more generous hard timeout
- early warning when Sledgehammer finds a proof
- another 'corec' example
- don't ask too much of 'transfer_prover'
- commented out for now
- tuning
- FIXME
- avoid 'prove_sorry' for unreliable tactics
- reused code
- tuning
- tuned examples
- new 'corec' example
- more reliable check for rhs variables
- strengthened tactic
- generalized ML function
- added '_legacy' suffixes
- generalized ML interface
- tuning
- refined experimental option of Sledgehammer