diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Thu Aug 09 18:12:15 2001 +0200
@@ -5,7 +5,7 @@
 \begin{isamarkuptext}%
 \noindent
 So far, all recursive definitions were shown to terminate via measure
-functions. Sometimes this can be quite inconvenient or even
+functions. Sometimes this can be inconvenient or
 impossible. Fortunately, \isacommand{recdef} supports much more
 general definitions. For example, termination of Ackermann's function
 can be shown by means of the \rmindex{lexicographic product} \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
@@ -25,18 +25,19 @@
 In general, \isacommand{recdef} supports termination proofs based on
 arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
 This is called \textbf{well-founded
-recursion}\indexbold{recursion!well-founded}. Clearly, a function definition
-is total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
+recursion}\indexbold{recursion!well-founded}.  A function definition
+is total if and only if the set of 
+all pairs $(r,l)$, where $l$ is the argument on the
 left-hand side of an equation and $r$ the argument of some recursive call on
 the corresponding right-hand side, induces a well-founded relation.  For a
 systematic account of termination proofs via well-founded relations see, for
 example, Baader and Nipkow~\cite{Baader-Nipkow}.
 
-Each \isacommand{recdef} definition should be accompanied (after the name of
-the function) by a well-founded relation on the argument type of the
-function.  Isabelle/HOL formalizes some of the most important
+Each \isacommand{recdef} definition should be accompanied (after the function's
+name) by a well-founded relation on the function's argument type.  
+Isabelle/HOL formalizes some of the most important
 constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
-example, \isa{measure\ f} is always well-founded, and the lexicographic
+example, \isa{measure\ f} is always well-founded.   The lexicographic
 product of two well-founded relations is again well-founded, which we relied
 on when defining Ackermann's function above.
 Of course the lexicographic product can also be iterated:%
@@ -54,8 +55,8 @@
 existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you
 will never have to prove well-foundedness of any relation composed
 solely of these building blocks. But of course the proof of
-termination of your function definition, i.e.\ that the arguments
-decrease with every recursive call, may still require you to provide
+termination of your function definition --- that the arguments
+decrease with every recursive call --- may still require you to provide
 additional lemmas.
 
 It is also possible to use your own well-founded relations with
@@ -76,7 +77,7 @@
 \begin{isamarkuptxt}%
 \noindent
 The proof is by showing that our relation is a subset of another well-founded
-relation: one given by a measure function.%
+relation: one given by a measure function.\index{*wf_subset (theorem)}%
 \end{isamarkuptxt}%
 \isacommand{apply}\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequote}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}%
 \begin{isamarkuptxt}%