--- a/src/HOL/Mirabelle/doc/options.txt Tue Oct 27 18:00:50 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-Options for sledgehammer:
-
- * prover=NAME: name of the external prover to call
- * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)
- * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed time)
- * 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=TIME: timeout for each minimization step (seconds of
- process time)
- * metis: apply metis with the theorems found by sledgehammer
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Oct 27 18:00:50 2009 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Oct 27 18:01:50 2009 +0100
@@ -35,8 +35,17 @@
echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:"
print_action_names
echo
- echo " A list of available OPTIONs can be found here:"
- echo " $MIRABELLE_HOME/doc/options.txt"
+ echo " Available OPTIONs for the ACTION sledgehammer:"
+ echo " * prover=NAME: name of the external prover to call"
+ echo " * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)"
+ echo " * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed"
+ echo " time)"
+ echo " * keep=PATH: path where to keep temporary files created by sledgehammer"
+ echo " * full_types: enable fully-typed encoding"
+ echo " * minimize: enable minimization of theorem set found by sledgehammer"
+ echo " * minimize_timeout=TIME: timeout for each minimization step (seconds of"
+ echo " process time)"
+ echo " * metis: apply metis to the theorems found by sledgehammer"
echo
echo " FILES is a list of theory files, where each file is either NAME.thy"
echo " or NAME.thy[START:END] and START and END are numbers indicating the"