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