--- a/doc-src/TutorialI/Inductive/document/AB.tex Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Fri Feb 16 06:46:20 2001 +0100
@@ -101,7 +101,7 @@
\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
integer 1 (see \S\ref{sec:numbers}).
-First we show that the our specific function, the difference between the
+First we show that our specific function, the difference between the
numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
move to the right. At this point we also start generalizing from \isa{a}'s
and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
@@ -114,7 +114,7 @@
\begin{isamarkuptxt}%
\noindent
The lemma is a bit hard to read because of the coercion function
-\isa{{\isachardoublequote}int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
+\isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns
a natural number, but subtraction on type~\isa{nat} will do the wrong thing.
Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which
@@ -222,7 +222,7 @@
\begin{isabelle}%
\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
\end{isabelle}
-With the help of \isa{part{\isadigit{1}}} it follows that
+With the help of \isa{part{\isadigit{2}}} it follows that
\begin{isabelle}%
\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
\end{isabelle}%