diff -r a1155e140597 -r 0f483b2632cd doc-src/TutorialI/Misc/document/simp.tex
--- 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.