--- a/doc-src/TutorialI/Documents/Documents.thy Sat Jan 05 01:20:52 2002 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Sat Jan 05 01:27:32 2002 +0100
@@ -246,7 +246,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,\,\verb,<yen>,, and \verb,$,.
Recall that a constructor like @{text Euro} actually is a function
@{typ "nat \<Rightarrow> currency"}. An expression like @{text "Euro 10"} will