--- a/doc-src/TutorialI/ToyList/ToyList.thy Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Jan 25 15:31:31 2001 +0100
@@ -177,7 +177,7 @@
txt{*\noindent\index{*induct_tac}%
This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
-@{term"tac"} stands for ``tactic'', a synonym for ``theorem proving function''.
+@{term"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 (@{term[source]Nil}) and the induction step
(@{term[source]Cons}):
@@ -207,7 +207,7 @@
txt{*\noindent
This command tells Isabelle to apply a proof strategy called
@{text"auto"} to all subgoals. Essentially, @{text"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 @{prop"rev [] = []"}) and disappears; the simplified version
of subgoal~2 becomes the new subgoal~1:
@{subgoals[display,indent=0,margin=70]}