diff -r fcff0c66b4f4 -r 08eee994bf99 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 04 19:19:29 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 04 19:19:51 2002 +0100
@@ -206,7 +206,7 @@
 \indexbold{definitions!unfolding}%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent