equal
deleted
inserted
replaced
19 grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \ |
19 grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \ |
20 perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/ $1$2/' |
20 perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/ $1$2/' |
21 } |
21 } |
22 |
22 |
23 function usage() { |
23 function usage() { |
|
24 # Do not forget to update the Sledgehammer documentation to reflect changes here. |
24 [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None" |
25 [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None" |
25 timeout="$MIRABELLE_TIMEOUT" |
26 timeout="$MIRABELLE_TIMEOUT" |
26 echo |
27 echo |
27 echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" |
28 echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" |
28 echo |
29 echo |
33 echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" |
34 echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" |
34 echo " -d DIR include session directory" |
35 echo " -d DIR include session directory" |
35 echo " -q be quiet (suppress output of Isabelle process)" |
36 echo " -q be quiet (suppress output of Isabelle process)" |
36 echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" |
37 echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" |
37 echo |
38 echo |
38 echo " Apply the given actions (i.e., automated proof tools)" |
39 echo " Apply the given actions at all proof steps in the given theory files." |
39 echo " at all proof steps in the given theory files." |
|
40 echo |
40 echo |
41 echo " ACTIONS is a colon-separated list of actions, where each action is" |
41 echo " ACTIONS is a colon-separated list of actions, where each action is" |
42 echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:" |
42 echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:" |
43 print_action_names |
43 print_action_names |
44 echo |
44 echo |