doc-src/Locales/Locales/document/isabelle.sty
changeset 25056 743f3603ba8b
parent 22649 6cf96b9f7b9e
child 25160 72fcf0832cfe
equal deleted inserted replaced
25055:3bb2ad8b1b37 25056:743f3603ba8b
    18 \newcommand{\isastylecmt}{\rm}
    18 \newcommand{\isastylecmt}{\rm}
    19 
    19 
    20 %symbol markup -- \emph achieves decent spacing via italic corrections
    20 %symbol markup -- \emph achieves decent spacing via italic corrections
    21 \newcommand{\isamath}[1]{\emph{$#1$}}
    21 \newcommand{\isamath}[1]{\emph{$#1$}}
    22 \newcommand{\isatext}[1]{\emph{#1}}
    22 \newcommand{\isatext}[1]{\emph{#1}}
    23 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    23 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    24 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    24 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    25 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    25 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    26 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    26 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    27 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    27 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    28 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
    28 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}