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