src/Doc/Sledgehammer/document/root.tex
 changeset 58090 f8ddde112e54 parent 57784 913b5dd101cb child 58497 20aaa307c0ff
equal inserted replaced
58089:20e76da3a0ef 58090:f8ddde112e54
   363 Options can be set globally using \textbf{sledgehammer\_params}
   363 Options can be set globally using \textbf{sledgehammer\_params}
   364 (\S\ref{command-syntax}). The command also prints the list of all available
   364 (\S\ref{command-syntax}). The command also prints the list of all available
   365 options with their current value. Fact selection can be influenced by specifying
   365 options with their current value. Fact selection can be influenced by specifying
   366 $(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call
   366 $(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call
   367 to ensure that certain facts are included, or simply $(\textit{my\_facts})$''
   367 to ensure that certain facts are included, or simply $(\textit{my\_facts})$''
   368 to force Sledgehammer to run only with $\textit{my\_facts}$.
   368 to force Sledgehammer to run only with $\textit{my\_facts}$ (and any facts

   369 chained into the goal).
   369
   370
   370 \section{Frequently Asked Questions}
   371 \section{Frequently Asked Questions}
   371 \label{frequently-asked-questions}
   372 \label{frequently-asked-questions}
   372
   373
   373 This sections answers frequently (and infrequently) asked questions about
   374 This sections answers frequently (and infrequently) asked questions about