doc-src/TutorialI/isabelle.sty
changeset 16585 02cf78f0afce
parent 16307 cb0f9e96d456
child 17056 05fc32a23b8b
equal deleted inserted replaced
16584:991ecdd985d9 16585:02cf78f0afce
    20 
    20 
    21 %symbol markup -- \emph achieves decent spacing via italic corrections
    21 %symbol markup -- \emph achieves decent spacing via italic corrections
    22 \newcommand{\isamath}[1]{\emph{$#1$}}
    22 \newcommand{\isamath}[1]{\emph{$#1$}}
    23 \newcommand{\isatext}[1]{\emph{#1}}
    23 \newcommand{\isatext}[1]{\emph{#1}}
    24 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    24 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    25 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    25 \newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
    26 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    26 \newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
    27 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    27 \newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
    28 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    28 \newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
    29 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
    29 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
    30 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
    30 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
    31 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
    31 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
    32 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
    32 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
    33 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    33 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}