diff -r 35f600d9bf06 -r 595da5b9854b doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Sun Nov 11 16:50:27 2007 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy	Sun Nov 11 16:50:29 2007 +0100
@@ -176,7 +176,7 @@
 (*>*)
 
 text {*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 @{text "(xsymbols)"}, is optional.
 
 We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in input, while