--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Oct 11 13:15:04 2000 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Oct 11 13:20:27 2000 +0200
@@ -39,7 +39,7 @@
Each \isacommand{recdef} definition should be accompanied (after the
name of the function) by a wellfounded relation on the argument type
-of the function. For example, \isa{measure} is defined by
+of the function. For example, \isaindexbold{measure} is defined by
\begin{isabelle}%
\ \ \ \ \ measure\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ f\ y\ {\isacharless}\ f\ x{\isacharbraceright}%
\end{isabelle}