diff -r d40cc6e7bfd8 -r aea72a834c85 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Thu Nov 29 21:12:37 2001 +0100
@@ -88,7 +88,10 @@
   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}%
+\end{warn}
+There is also a growing Library~\cite{isabelle-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.%
 \index{theories|)}