diff -r 449e1a1bb7a8 -r d848c6693185 doc-src/TutorialI/Inductive/document/AB.tex
--- 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}%