
diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Inductive/document/AB.tex
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Thu Aug 09 18:12:15 2001 +0200
@@ -7,6 +7,7 @@
 %
 \begin{isamarkuptext}%
 \label{sec:CFG}
+\index{grammars!defining inductively|(}%
 Grammars are nothing but shorthands for inductive definitions of nonterminals
 which represent sets of strings. For example, the production
 $A \to B c$ is short for
@@ -129,8 +130,7 @@
 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
 \begin{isamarkuptext}%
-Finally we come to the above mentioned lemma about cutting in half a word with two
-more elements of one sort than of the other sort:%
+Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
 \ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline
@@ -199,7 +199,7 @@
 holds for all words shorter than \isa{w}.
 
 The proof continues with a case distinction on \isa{w},
-i.e.\ if \isa{w} is empty or not.%
+on whether \isa{w} is empty or not.%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
@@ -266,7 +266,9 @@
 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
 \begin{isamarkuptext}%
 We conclude this section with a comparison of our proof with 
-Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook
+Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
+\cite[p.\ts81]{HopcroftUllman}.
+For a start, the textbook
 grammar, for no good reason, excludes the empty word, thus complicating
 matters just a little bit: they have 8 instead of our 7 productions.
 
@@ -283,8 +285,9 @@
 thus is not at all similar to the other cases (which are automatic in
 Isabelle). The authors are at least cavalier about this point and may
 even have overlooked the slight difficulty lurking in the omitted
-cases. This is not atypical for pen-and-paper proofs, once analysed in
-detail.%
+cases.  Such errors are found in many pen-and-paper proofs when they
+are scrutinized formally.%
+\index{grammars!defining inductively|)}%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:




