--- a/src/HOL/Mirabelle/doc/options.txt Sat Sep 05 17:35:05 2009 +0200
+++ b/src/HOL/Mirabelle/doc/options.txt Sat Sep 05 22:01:31 2009 +0200
@@ -2,5 +2,7 @@
* prover=NAME: name of the external prover to call
* keep=PATH: path where to keep temporary files created by sledgehammer
+ * full_types: enable full-typed encoding
+ * minimize: enable minimization of theorem set found by sledgehammer
+ * minimize_timeout: timeout for each minimization step
* metis: apply metis with the theorems found by sledgehammer
- * full_types: turn on full-typed encoding