--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Sat Apr 14 23:52:17 2012 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Sat Apr 14 23:52:17 2012 +0100
@@ -15,6 +15,11 @@
done
}
+function print_sledgehammer_options() {
+ grep -e "^val .*K =" $MIRABELLE_HOME/Actions/mirabelle_sledgehammer.ML \
+ | perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/ $1$2/'
+}
+
function usage() {
[ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"
timeout="$MIRABELLE_TIMEOUT"
@@ -36,18 +41,7 @@
print_action_names
echo
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 " * metis_ft: apply metis with fully-typed encoding to the theorems found"
- echo " by sledgehammer"
+ print_sledgehammer_options
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"