diff -r 140241dc55e6 -r 40fbd988b59b doc-src/TutorialI/Documents/Documents.thy
--- 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