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