--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Dec 01 20:24:08 2000 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Mon Dec 04 17:29:48 2000 +0100
@@ -25,9 +25,8 @@
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}\index{well-founded
-recursion|see{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}. Clearly, a function definition
+is total iff 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