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