changeset 10190 871772d38b30
parent 10189 865918597b63
child 10241 e0428c2778f1
--- 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.