1.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Mon Oct 23 17:36:09 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Mon Oct 23 17:37:03 2000 +0200
     1.3 @@ -21,13 +21,13 @@
     1.4  At the end we say a few words about the relationship of the formalization
     1.5  and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
     1.6  
     1.7 -We start by fixing the alpgabet, which consists only of \isa{a}'s
     1.8 +We start by fixing the alphabet, which consists only of \isa{a}'s
     1.9  and \isa{b}'s:%
    1.10  \end{isamarkuptext}%
    1.11  \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
    1.12  \begin{isamarkuptext}%
    1.13  \noindent
    1.14 -For convenience we includ the following easy lemmas as simplification rules:%
    1.15 +For convenience we include the following easy lemmas as simplification rules:%
    1.16  \end{isamarkuptext}%
    1.17  \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline
    1.18  \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline