# HG changeset patch
# User boehmes
# Date 1256662910 -3600
# Node ID 95478a5b4c051cba76d4557f55353d7e7537b9a9
# Parent  ed1681284f624e51afb322217932c858902a84c3
included description for sledgehammer options in Mirabelle script

diff -r ed1681284f62 -r 95478a5b4c05 src/HOL/Mirabelle/doc/options.txt
--- 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
diff -r ed1681284f62 -r 95478a5b4c05 src/HOL/Mirabelle/lib/Tools/mirabelle
--- 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"