--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/doc/options.txt	Tue Sep 01 14:09:59 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)