doc-src/TutorialI/Misc/document/simp.tex
changeset 12627 08eee994bf99
parent 12584 cf5a342ce698
child 13623 c2b235e60f8b
--- 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