--- a/doc-src/TutorialI/basics.tex Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/basics.tex Wed Dec 12 09:04:20 2001 +0100
@@ -89,9 +89,9 @@
Unless you know what you are doing, always include \isa{Main}
as a direct or indirect parent of all your theories.
\end{warn}
-There is also a growing Library~\cite{isabelle-library}\index{Library}
+There is also a growing Library~\cite{HOL-Library}\index{Library}
of useful theories that are not part of \isa{Main} but can to be included
-among the parents of a theory and will then be included automatically.%
+among the parents of a theory and will then be loaded automatically.%
\index{theories|)}