diff -r ca83cc2973f9 -r 0d2a6feeb634 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Wed Sep 20 00:02:26 2000 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Wed Sep 20 00:50:09 2000 +0200
@@ -91,11 +91,15 @@
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 
 
-% alternative styles -- default is "tt"
+% alternative styles
 
 \newcommand{\isabellestyle}{}
 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
 
+\newcommand{\isabellestylett}{%
+\renewcommand{\isastyle}{\small\tt}%
+\renewcommand{\isastyleminor}{\tt}%
+}
 \newcommand{\isabellestyleit}{%
 \renewcommand{\isastyle}{\small\it}%
 \renewcommand{\isastyleminor}{\it}%