doc-src/TutorialI/Misc/simp.thy

 
 \begin{warn}
 Always use ``\texttt{\_}'' rather than variable names: searching for
 \texttt{"x + y"} will usually not find any matching theorems
 because they would need to contain \texttt{x} and~\texttt{y} literally.
-
 When searching for infix operators, do not just type in the symbol,
 such as~\texttt{+}, but a proper term such as \texttt{"_ + _"}.
 This remark applies to more complicated syntaxes, too.
 \end{warn}