
diff -r 279da0358aa9 -r 09a6c44a48ea doc-src/TutorialI/Sets/sets.tex
--- 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}.




