diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/ToyList/document/ToyList.tex --- 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}.