--- a/doc-src/TutorialI/Sets/sets.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex Fri Aug 03 18:04:55 2001 +0200
@@ -892,7 +892,8 @@
formulations are all complicated. However, often a relation
is well-founded by construction. HOL provides
theorems concerning ways of constructing a well-founded relation. The
-most familiar way is to specify a \bfindex{measure function}~\isa{f} into
+most familiar way is to specify a
+\index{measure functions}\textbf{measure function}~\isa{f} into
the natural numbers, when $\isa{x}\prec \isa{y}\iff \isa{f x} < \isa{f y}$;
we write this particular relation as
\isa{measure~f}.