equal
deleted
inserted
replaced
17 \renewcommand{\nomname}{\glossaryname} |
17 \renewcommand{\nomname}{\glossaryname} |
18 \renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}} |
18 \renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}} |
19 |
19 |
20 %% index |
20 %% index |
21 \newcommand{\indexml}[1]{\index{\emph{#1}|bold}} |
21 \newcommand{\indexml}[1]{\index{\emph{#1}|bold}} |
|
22 \newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}} |
22 \newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}} |
23 \newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}} |
23 \newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}} |
24 \newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}} |
24 \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}} |
25 \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}} |
25 |
26 |
26 %% math |
27 %% math |