diff -r d40cc6e7bfd8 -r aea72a834c85 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Thu Nov 29 21:12:37 2001 +0100
@@ -965,8 +965,8 @@
 the well-founded relation used to prove termination.
 
 The \bfindex{multiset ordering}, useful for hard termination proofs, is
-available in the Library.  Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow}
-discuss it. 
+available in the Library~\cite{isabelle-HOL-lib}.
+Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow} discuss it. 
 
 \medskip
 Induction\index{induction!well-founded|(}