# HG changeset patch
# User nipkow
# Date 975599318 -3600
# Node ID 2163888487861b282af6342b3cfeab4d3c1877a2
# Parent  71eb53f36878a862642f54959cba507bf95ee3ba
*** empty log message ***

diff -r 71eb53f36878 -r 216388848786 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Thu Nov 30 14:10:23 2000 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Thu Nov 30 16:48:38 2000 +0100
@@ -23,9 +23,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