diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Jul 31 17:42:38 2002 +0200
@@ -118,7 +118,7 @@
   output as @{text "A\<^sup>\<star>"}.
 
   \medskip Replacing our definition of @{text xor} by the following
-  specifies a Isabelle symbol for the new operator:
+  specifies an Isabelle symbol for the new operator:
 *}
 
 (*<*)