notation works with any known constant (including fixes/abbrevs);
authorwenzelm
Sun, 11 Nov 2007 16:50:29 +0100 (2007-11-11)
changeset 25399 595da5b9854b
parent 25398 35f600d9bf06
child 25400 e05b9fa43885
notation works with any known constant (including fixes/abbrevs);
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