doc-src/IsarRef/style.sty
changeset 28760 cbc435f7b16b
parent 28758 4ce896a30f88
child 28763 b5e6122ff575
equal deleted inserted replaced
28759:8358fabeea95 28760:cbc435f7b16b
    14 \newcommand{\appref}[1]{appendix~\ref{#1}}
    14 \newcommand{\appref}[1]{appendix~\ref{#1}}
    15 \newcommand{\Appref}[1]{Appendix~\ref{#1}}
    15 \newcommand{\Appref}[1]{Appendix~\ref{#1}}
    16 \newcommand{\figref}[1]{figure~\ref{#1}}
    16 \newcommand{\figref}[1]{figure~\ref{#1}}
    17 \newcommand{\Figref}[1]{Figure~\ref{#1}}
    17 \newcommand{\Figref}[1]{Figure~\ref{#1}}
    18 
    18 
    19 %% index
    19 %% ML
    20 \newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
    20 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
    21 \newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
    21 \newcommand{\indexml}[1]{\index{#1 (ML value)|bold}}
    22 \newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
       
    23 \newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
       
    24 \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
       
    25 
    22 
    26 %% math
    23 %% math
    27 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
    24 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
    28 \renewcommand{\isadigit}[1]{\isamath{#1}}
    25 \renewcommand{\isadigit}[1]{\isamath{#1}}
    29 
    26