diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -122,7 +122,7 @@
   output as \isa{A\isactrlsup {\isasymstar}}.
 
   \medskip Replacing our definition of \isa{xor} by the following
-  specifies a Isabelle symbol for the new operator:%
+  specifies an Isabelle symbol for the new operator:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%