# HG changeset patch # User wenzelm # Date 1192710655 -7200 # Node ID aabaab4ad212d9a50b2dd30c493fb66237580d1a # Parent 21d44e3aea4ccedd5957febf03a12b73593ff9fa DeclareRobustCommand \isactrlbsub/esub etc.; diff -r 21d44e3aea4c -r aabaab4ad212 lib/texinputs/isabelle.sty --- a/lib/texinputs/isabelle.sty Thu Oct 18 09:21:00 2007 +0200 +++ b/lib/texinputs/isabelle.sty Thu Oct 18 14:30:55 2007 +0200 @@ -25,10 +25,10 @@ \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} +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript} +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript} +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}