# HG changeset patch
# User wenzelm
# Date 1194796229 -3600
# Node ID 595da5b9854b8e2a843202ba547fee05d74928df
# Parent  35f600d9bf06296a688244536ed534325fa5c8fc
notation works with any known constant (including fixes/abbrevs);

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