diff -r 6decc1ffdbed -r 4ab00a2642c3 src/HOL/Mirabelle/doc/options.txt
--- /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)