--- a/src/HOL/Mirabelle/doc/options.txt Sat Sep 05 11:45:57 2009 +0200
+++ b/src/HOL/Mirabelle/doc/options.txt Sat Sep 05 15:46:52 2009 +0200
@@ -2,6 +2,5 @@
* 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)
- * full_types=X: turn on full-typed encoding (X may be any non-empty string)
+ * metis: apply metis with the theorems found by sledgehammer
+ * full_types: turn on full-typed encoding