--- a/doc-src/TutorialI/Advanced/WFrec.thy Wed Oct 11 13:15:04 2000 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Wed Oct 11 13:20:27 2000 +0200
@@ -37,7 +37,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, @{term measure} is defined by
+of the function. For example, \isaindexbold{measure} is defined by
@{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"}
and it has been proved that @{term"measure f"} is always wellfounded.
--- 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}