--- a/doc-src/TutorialI/isabelle.sty Wed Oct 22 10:52:36 2003 +0200
+++ b/doc-src/TutorialI/isabelle.sty Wed Oct 22 10:53:12 2003 +0200
@@ -24,6 +24,8 @@
\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
\newdimen\isa@parindent\newdimen\isa@parskip