changeset 32496 | 4ab00a2642c3 |
parent 32469 | 1ad7d4fc0954 |
child 32511 | 43d2ac4aa2de |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/doc/options.txt Wed Sep 02 16:23:53 2009 +0200 @@ -0,0 +1,6 @@ +Options for sledgehammer: + + * prover=NAME: name of the external prover to call + * keep=PATH: path where to keep temporary files created by sledgehammer + * metis=X: apply metis with the theorems found by sledgehammer (X may be any + non-empty string)