--- 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}%