# HG changeset patch
# User blanchet
# Date 1306485007 -7200
# Node ID bb212c2ad2380ba2f356ee7268a44175be093fdf
# Parent  b48aa3492f0ba19de6ac9525552f47fcef5791c9
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise

diff -r b48aa3492f0b -r bb212c2ad238 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
@@ -250,34 +250,33 @@
 Sledgehammer: ``\textit{e}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
-To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
-To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis list.inject}). \\
-To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
 %
 %Sledgehammer: ``\textit{remote\_waldmeister}'' for subgoal 1: \\
 %$[a] = [b] \,\Longrightarrow\, a = b$ \\
 %Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
-%To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_waldmeister}] \\
+%To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_waldmeister}] \\
 %\phantom{\textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
-To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}] \\
-\phantom{To minimize: }(\textit{hd.simps}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
-To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_z3}]~(\textit{hd.simps}).
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_z3}]~(\textit{hd.simps}).
 \postw
 
 Sledgehammer ran E, SInE-E, SPASS, Vampire, %Waldmeister,
@@ -411,7 +410,7 @@
 very seldom be an issue, but if you notice many unsound proofs, contact the
 author at \authoremail.
 
-\point{How can I tell whether a Sledgehammer proof is sound?}
+\point{How can I tell whether a generated proof is sound?}
 
 First, if \emph{metis} (or \emph{metisFT}) can reconstruct it, the proof is
 sound (modulo soundness of Isabelle's inference kernel). If it fails or runs
@@ -423,7 +422,7 @@
 \postw
 
 where \textit{metis\_facts} is the list of facts appearing in the suggested
-Metis call. The automatic provers should be able to refind the proof very
+Metis call. The automatic provers should be able to re-find the proof very
 quickly if it is sound, and the \textit{type\_sys} $=$ \textit{poly\_tags}
 option (\S\ref{problem-encoding}) ensures that no unsound proofs are found.
 
@@ -436,13 +435,12 @@
 \textbf{sledgehammer} [\textit{full\_types}] (\textit{nat.distinct\/}(1))
 \postw
 
-\point{How does Sledgehammer select the facts that should be passed to the
-automatic provers?}
+\point{Which facts are passed to the automatic provers?}
 
-Briefly, the relevance filter assigns a score to every available fact (lemma,
-theorem, definition, or axiom)\ based upon how many constants that fact shares
-with the conjecture. This process iterates to include facts relevant to those
-just accepted, but with a decay factor to ensure termination. The constants are
+The relevance filter assigns a score to every available fact (lemma, theorem,
+definition, or axiom)\ based upon how many constants that fact shares with the
+conjecture. This process iterates to include facts relevant to those just
+accepted, but with a decay factor to ensure termination. The constants are
 weighted to give unusual ones greater significance. The relevance filter copes
 best when the conjecture contains some unusual constants; if all the constants
 are common, it is unable to discriminate among the hundreds of facts that are
@@ -450,7 +448,7 @@
 how many times a particular fact has been used in a proof, and it cannot learn.
 
 The number of facts included in a problem varies from prover to prover, since
-some provers get overwhelmed quicker than others. You can show the number of
+some provers get overwhelmed more easily than others. You can show the number of
 facts given using the \textit{verbose} option (\S\ref{output-format}) and the
 actual facts using \textit{debug} (\S\ref{output-format}).
 
@@ -487,7 +485,7 @@
 \textbf{sledgehammer}
 \postw
 
-\point{Why are the Isar proofs generated by Sledgehammer so ugly?}
+\point{Why are the generated Isar proofs so ugly/detailed/broken?}
 
 The current implementation is experimental and explodes exponentially in the
 worst case. Work on a new implementation has begun. There is a large body of
@@ -496,20 +494,20 @@
 set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
 value or to try several provers and keep the nicest-looking proof.
 
-\point{Should I let Sledgehammer minimize the number of lemmas?}
+\point{Should I minimize the number of lemmas?}
 
 In general, minimization is a good idea, because proofs involving fewer lemmas
 tend to be shorter as well, and hence easier to re-find by Metis. But the
 opposite is sometimes the case.
 
-\point{Why does the minimizer sometimes starts of its own?}
+\point{Why does the minimizer sometimes starts on its own?}
 
 There are two scenarios in which this can happen. First, some provers (notably
 CVC3, Satallax, and Yices) do not provide proofs or sometimes provide incomplete
 proofs. The minimizer is then invoked to find out which facts are actually
 needed from the (large) set of facts that was initinally given to the prover.
 Second, if a prover returns a proof with lots of facts, the minimizer is invoked
-automatically since Metis is unlikely to refind the proof.
+automatically since Metis would be unlikely to re-find the proof.
 
 \point{What is metisFT?}
 
@@ -531,7 +529,7 @@
 in a successful Metis proof, you can advantageously replace the \textit{metis}
 call with \textit{metisFT}.
 
-\point{I got a strange error from Sledgehammer---what should I do?}
+\point{A strange error occurred---what should I do?}
 
 Sledgehammer tries to give informative error messages. Please report any strange
 error to the author at \authoremail. This applies double if you get the message
@@ -580,7 +578,7 @@
 \item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on
 subgoal number \textit{num} (1 by default), with the given options and facts.
 
-\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
+\item[$\bullet$] \textbf{\textit{min}:} Attempts to minimize the provided facts
 (specified in the \textit{facts\_override} argument) to obtain a simpler proof
 involving fewer facts. The options and goal number are as for \textit{run}.
 
diff -r b48aa3492f0b -r bb212c2ad238 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
@@ -283,7 +283,7 @@
 val sledgehammer_paramsN = "sledgehammer_params"
 
 val runN = "run"
-val minimizeN = "minimize"
+val minN = "min"
 val messagesN = "messages"
 val supported_proversN = "supported_provers"
 val running_proversN = "running_provers"
@@ -296,7 +296,7 @@
   key ^ (case implode_param values of "" => "" | value => " = " ^ value)
 
 fun minimize_command override_params i prover_name fact_names =
-  sledgehammerN ^ " " ^ minimizeN ^ " [prover = " ^ prover_name ^
+  sledgehammerN ^ " " ^ minN ^ " [prover = " ^ prover_name ^
   (override_params |> filter is_raw_param_relevant_for_minimize
                    |> implode o map (prefix ", " o string_for_raw_param)) ^
   "] (" ^ space_implode " " fact_names ^ ")" ^
@@ -315,7 +315,7 @@
                          state
         |> K ()
       end
-    else if subcommand = minimizeN then
+    else if subcommand = minN then
       run_minimize (get_params false ctxt override_params) (the_default 1 opt_i)
                    (#add relevance_override) state
     else if subcommand = messagesN then