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