diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Fri Jan 12 16:07:20 2001 +0100
@@ -30,11 +30,11 @@
 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, \cite{Baader-Nipkow}.
+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.  The HOL library formalizes some of the most important
+function.  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
 product of two well-founded relations is again well-founded, which we relied
@@ -50,7 +50,7 @@
 {\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}%
 \begin{isamarkuptext}%
 Lexicographic products of measure functions already go a long
-way. Furthermore you may embed some type in an
+way. Furthermore, you may embed a type in an
 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