--- 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