diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Jan 25 15:31:31 2001 +0100
@@ -172,7 +172,7 @@
 \begin{isamarkuptxt}%
 \noindent\index{*induct_tac}%
 This tells Isabelle to perform induction on variable \isa{xs}. The suffix
-\isa{tac} stands for ``tactic'', a synonym for ``theorem proving function''.
+\isa{tac} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
 By default, induction acts on the first subgoal. The new proof state contains
 two subgoals, namely the base case (\isa{Nil}) and the induction step
 (\isa{Cons}):
@@ -204,7 +204,7 @@
 \noindent
 This command tells Isabelle to apply a proof strategy called
 \isa{auto} to all subgoals. Essentially, \isa{auto} tries to
-``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
+simplify the subgoals.  In our case, subgoal~1 is solved completely (thanks
 to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
 of subgoal~2 becomes the new subgoal~1:
 \begin{isabelle}%