diff -r e05b9fa43885 -r 5f818e7a46b5 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Sun Nov 11 16:50:30 2007 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Sun Nov 11 16:58:41 2007 +0100
@@ -205,7 +205,7 @@
 \ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
 \begin{isamarkuptext}%
 The \commdx{notation} command associates a mixfix
-annotation with a logical constant.  The print mode specification of
+annotation with a known constant.  The print mode specification of
 \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional.
 
 We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while