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