diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Nov 29 13:33:45 2001 +0100
@@ -18,8 +18,8 @@
 %
 \begin{isamarkuptext}%
 \noindent
-\index{datatype@\isacommand {datatype} (command)}
-The datatype \tydx{list} introduces two
+The datatype\index{datatype@\isacommand {datatype} (command)}
+\tydx{list} introduces two
 constructors \cdx{Nil} and \cdx{Cons}, the
 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
@@ -150,7 +150,7 @@
 \isa{xs}.
 \end{itemize}
 The name and the simplification attribute are optional.
-Isabelle's response is to print
+Isabelle's response is to print the initial proof state
 \begin{isabelle}
 proof(prove):~step~0\isanewline
 \isanewline
@@ -200,7 +200,7 @@
 
 The induction step is an example of the general format of a subgoal:\index{subgoals}
 \begin{isabelle}
-~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
+~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
 ignored most of the time, or simply treated as a list of variables local to