--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Jul 18 15:49:34 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Tue Jul 19 11:38:45 2005 +0200
@@ -530,7 +530,6 @@
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.