diff -r 5b6305cab436 -r 9feb1e0c4cb3 doc-src/TutorialI/basics.tex
--- 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}