equal
deleted
inserted
replaced
|
1 Options for sledgehammer: |
|
2 |
|
3 * prover=NAME: name of the external prover to call |
|
4 * keep=PATH: path where to keep temporary files created by sledgehammer |
|
5 * metis=X: apply metis with the theorems found by sledgehammer (X may be any |
|
6 non-empty string) |