--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Oct 25 17:44:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Oct 25 18:24:33 2000 +0200
@@ -179,8 +179,8 @@
The induction step is an example of the general format of a subgoal:
\begin{isabelle}
-~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
-\end{isabelle}
+~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
+\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
ignored most of the time, or simply treated as a list of variables local to
this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.