diff -r d25be0ad1a6c -r 1b02a6c4032f doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Jul 23 19:06:11 2001 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Jul 24 11:25:54 2001 +0200
@@ -21,16 +21,16 @@
 empty~list and the operator that adds an element to the front of a list. For
 example, the term \isa{Cons True (Cons False Nil)} is a value of
 type \isa{bool\ list}, namely the list with the elements \isa{True} and
-\isa{False}. Because this notation becomes unwieldy very quickly, the
+\isa{False}. Because this notation quickly becomes unwieldy, the
 datatype declaration is annotated with an alternative syntax: instead of
 \isa{Nil} and \isa{Cons x xs} we can write
 \isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and
 \isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
-alternative syntax is the standard syntax. Thus the list \isa{Cons True
+alternative syntax is the familiar one.  Thus the list \isa{Cons True
 (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 
 means that \isa{{\isacharhash}} associates to
-the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
+the right: the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
 The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.