# HG changeset patch # User paulson # Date 972315487 -7200 # Node ID 74be38751d067ec591c7a787994077d3935852a6 # Parent 8a5aa26c125fc43911048bd3fb52a5d85aee43fa fixed crossref diff -r 8a5aa26c125f -r 74be38751d06 doc-src/TutorialI/ToyList/ToyList.thy --- a/doc-src/TutorialI/ToyList/ToyList.thy Mon Oct 23 17:37:49 2000 +0200 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Mon Oct 23 17:38:07 2000 +0200 @@ -188,7 +188,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 Chapter~\ref{ch:Rules}. +this subgoal. Their deeper significance is explained in Chapter~\ref{chap: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