diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -965,7 +965,7 @@
 the well-founded relation used to prove termination.
 
 The \bfindex{multiset ordering}, useful for hard termination proofs, is
-available in the Library~\cite{isabelle-HOL-lib}.
+available in the Library~\cite{HOL-Library}.
 Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow} discuss it. 
 
 \medskip