1.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Fri May 18 17:18:43 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Sat May 19 12:19:23 2001 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4  \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
     1.5  \begin{isamarkuptext}%
     1.6  We conclude this section with a comparison of our proof with 
     1.7 -Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook
     1.8 +Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook
     1.9  grammar, for no good reason, excludes the empty word, thus complicating
    1.10  matters just a little bit: they have 8 instead of our 7 productions.
    1.11