
diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Oct 25 17:44:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Oct 25 18:24:33 2000 +0200
@@ -184,8 +184,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}.




