--- 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
@@ -461,6 +461,34 @@
number of facts, by setting the \textit{max\_relevant} option
(\S\ref{relevance-filter}) to, say, 50 or 100.
+You can also influence which facts are actually selected in a number of ways. If
+you simply want to ensure that a fact is included, you can specify it using the
+``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example:
+%
+\prew
+\textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps})
+\postw
+%
+The specified facts then replace the least relevant facts that would otherwise be
+included; the other selected facts remain the same.
+If you want to direct the selection in a particular direction, you can specify
+the facts via \textbf{using}:
+%
+\prew
+\textbf{using} \textit{hd.simps} \textit{tl.simps} \\
+\textbf{sledgehammer}
+\postw
+%
+The facts are then more likely to be selected than otherwise, and if they are
+selected at iteration $j$ they also influence which facts are selected at
+iterations $j + 1$, $j + 2$, etc. To give them even more weight, try
+%
+\prew
+\textbf{using} \textit{hd.simps} \textit{tl.simps} \\
+\textbf{apply}~\textbf{--} \\
+\textbf{sledgehammer}
+\postw
+
\point{Why are the Isar proofs generated by Sledgehammer so ugly?}
The current implementation is experimental and explodes exponentially in the
@@ -478,11 +506,11 @@
\point{Why does the minimizer sometimes starts of its own?}
-There are two scenarios in which this can happen. First, some provers (e.g.,
-CVC3 and Yices) do not provide proofs or 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
+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.
\point{What is metisFT?}