src/Doc/Sledgehammer/document/root.tex
changeset 58090 f8ddde112e54
parent 57784 913b5dd101cb
child 58497 20aaa307c0ff
equal deleted 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