diff -r 140241dc55e6 -r 40fbd988b59b doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Sat Jan 05 01:20:52 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Sat Jan 05 01:27:32 2002 +0100
@@ -244,7 +244,7 @@
 Here the degenerate mixfix annotations on the rightmost column
   happen to consist of a single Isabelle symbol each:
   \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
-  \verb,\,\verb,<yen>,, and \verb,\,\verb,<dollar>,.
+  \verb,\,\verb,<yen>,, and \verb,$,.
 
   Recall that a constructor like \isa{Euro} actually is a function
   \isa{nat\ {\isasymRightarrow}\ currency}.  An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will