doc-src/TutorialI/ToyList/document/ToyList.tex
changeset 10236 7626cb4e1407
parent 10187 0376cccd9118
child 10299 8627da9246da
     1.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Oct 17 10:45:51 2000 +0200
     1.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Oct 17 13:28:57 2000 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4  \end{isabelle}
     1.5  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
     1.6  ignored most of the time, or simply treated as a list of variables local to
     1.7 -this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
     1.8 +this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}.
     1.9  The {\it assumptions} are the local assumptions for this subgoal and {\it
    1.10    conclusion} is the actual proposition to be proved. Typical proof steps
    1.11  that add new assumptions are induction or case distinction. In our example