# HG changeset patch
# User blanchet
# Date 1409249219 -7200
# Node ID f8ddde112e5492a3a753dbca71d2cad56202c1e2
# Parent  20e76da3a0efc722e7913416333b9c7ed9f91827
clarified docs

diff -r 20e76da3a0ef -r f8ddde112e54 src/Doc/Sledgehammer/document/root.tex
--- 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}