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}.