diff -r 20cf817f3b4a -r 7626cb4e1407 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Oct 17 10:45:51 2000 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Oct 17 13:28:57 2000 +0200 @@ -183,7 +183,7 @@ \end{isabelle} 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 \S\ref{sec:PCproofs}. +this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}. The {\it assumptions} are the local assumptions for this subgoal and {\it conclusion} is the actual proposition to be proved. Typical proof steps that add new assumptions are induction or case distinction. In our example