equal
deleted
inserted
replaced
1 Options for sledgehammer: |
|
2 |
|
3 * prover=NAME: name of the external prover to call |
|
4 * prover_timeout=TIME: timeout for invoked ATP (seconds of process time) |
|
5 * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed time) |
|
6 * keep=PATH: path where to keep temporary files created by sledgehammer |
|
7 * full_types: enable full-typed encoding |
|
8 * minimize: enable minimization of theorem set found by sledgehammer |
|
9 * minimize_timeout=TIME: timeout for each minimization step (seconds of |
|
10 process time) |
|
11 * metis: apply metis with the theorems found by sledgehammer |
|