diff -r 494f8cd34df7 -r 44fefb6e9994 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 02 11:30:38 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 02 13:17:11 2000 +0200
@@ -209,8 +209,9 @@
 \begin{isamarkuptext}%
 \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
 
-After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type
-\isacommand{oops}) we start a new proof:%
+After abandoning the above proof attempt\indexbold{abandon
+proof}\indexbold{proof!abandon} (at the shell level type
+\isacommand{oops}\indexbold{*oops}) we start a new proof:%
 \end{isamarkuptext}%
 \isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}%
 \begin{isamarkuptxt}%