--- a/src/Doc/Sledgehammer/document/root.tex Thu Aug 28 20:05:39 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Aug 28 20:06:59 2014 +0200
@@ -365,7 +365,8 @@
options with their current value. Fact selection can be influenced by specifying
``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call
to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$''
-to force Sledgehammer to run only with $\textit{my\_facts}$.
+to force Sledgehammer to run only with $\textit{my\_facts}$ (and any facts
+chained into the goal).
\section{Frequently Asked Questions}
\label{frequently-asked-questions}