# HG changeset patch
# User paulson
# Date 1084265235 -7200
# Node ID 967db86e853cb980c17ed09b4980cb20adb66282
# Parent  5670fc027a3b4298e175be6a5b626c2648449e8e
auto update

diff -r 5670fc027a3b -r 967db86e853c doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Mon May 10 19:27:45 2004 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Tue May 11 10:47:15 2004 +0200
@@ -26,15 +26,12 @@
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
+\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
-% somewhat hackish: spanning sub/super scripts (\<^bsub>..\<^esub>)
-\newcommand{\isactrlbsub}{%
-\def\isatext##1{\isastylescript##1}\begin{math}_\bgroup}
-\newcommand{\isactrlesub}{\egroup\end{math}}
-\newcommand{\isactrlbsup}{%
-\def\isatext##1{\isastylescript##1}\begin{math}^\bgroup}
-\newcommand{\isactrlesup}{\egroup\end{math}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip