doc-src/TutorialI/ToyList/ToyList.thy
changeset 10236 7626cb4e1407
parent 10171 59d6633835fa
child 10302 74be38751d06
     1.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Tue Oct 17 10:45:51 2000 +0200
     1.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Oct 17 13:28:57 2000 +0200
     1.3 @@ -40,8 +40,8 @@
     1.4  Next, two functions @{text"app"} and \isaindexbold{rev} are declared:
     1.5  *}
     1.6  
     1.7 -consts app :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list"   (infixr "@" 65)
     1.8 -       rev :: "'a list \\<Rightarrow> 'a list";
     1.9 +consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   (infixr "@" 65)
    1.10 +       rev :: "'a list \<Rightarrow> 'a list";
    1.11  
    1.12  text{*
    1.13  \noindent
    1.14 @@ -100,7 +100,7 @@
    1.15  dropped, unless the identifier happens to be a keyword, as in
    1.16  *}
    1.17  
    1.18 -consts "end" :: "'a list \\<Rightarrow> 'a"
    1.19 +consts "end" :: "'a list \<Rightarrow> 'a"
    1.20  
    1.21  text{*\noindent
    1.22  When Isabelle prints a syntax error message, it refers to the HOL syntax as
    1.23 @@ -188,7 +188,7 @@
    1.24  \end{isabelle}
    1.25  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
    1.26  ignored most of the time, or simply treated as a list of variables local to
    1.27 -this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
    1.28 +this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}.
    1.29  The {\it assumptions} are the local assumptions for this subgoal and {\it
    1.30    conclusion} is the actual proposition to be proved. Typical proof steps
    1.31  that add new assumptions are induction or case distinction. In our example