--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Mar 07 15:54:11 2001 +0100
@@ -34,7 +34,7 @@
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. HOL formalizes some of the most important
+function. 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
product of two well-founded relations is again well-founded, which we relied
@@ -74,6 +74,7 @@
\end{isamarkuptext}%
\isacommand{lemma}\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
\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.%
\end{isamarkuptxt}%