src/HOL/Mirabelle/doc/options.txt
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)