doc-src/TutorialI/basics.tex

   HOL contains a theory \thydx{Main}, the union of all the basic
   predefined theories like arithmetic, lists, sets, etc.  
   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|)}
 
 
 \section{Types, Terms and Formulae}
 \label{sec:TypesTermsForms}