--- a/doc-src/TutorialI/basics.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/basics.tex Tue Sep 12 15:43:15 2000 +0200
@@ -73,7 +73,7 @@
\begin{warn}
HOL contains a theory \isaindexbold{Main}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.\ (see the online
- library). Unless you know what you are doing, always include \texttt{Main}
+ library). Unless you know what you are doing, always include \isa{Main}
as a direct or indirect parent theory of all your theories.
\end{warn}