1.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Tue Nov 07 18:38:24 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Wed Nov 08 14:38:04 2000 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4  \end{isabelle}
     1.5  where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
     1.6  \isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
     1.7 -integer 1 (see \S\ref{sec:int}).
     1.8 +integer 1 (see \S\ref{sec:numbers}).
     1.9  
    1.10  First we show that the our specific function, the difference between the
    1.11  numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
    1.12 @@ -115,7 +115,7 @@
    1.13  \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
    1.14  \ \ \ \ \ \ {\isacharminus}\isanewline
    1.15  \ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
    1.16 -\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
    1.17 +\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
    1.18  \begin{isamarkuptxt}%
    1.19  \noindent
    1.20  The lemma is a bit hard to read because of the coercion function