doc-src/IsarImplementation/style.sty
changeset 18554 bff7a1466fe4
parent 18537 2681f9e34390
child 20024 553d48cac687
     1.1 --- a/doc-src/IsarImplementation/style.sty	Tue Jan 03 11:57:33 2006 +0100
     1.2 +++ b/doc-src/IsarImplementation/style.sty	Tue Jan 03 13:59:55 2006 +0100
     1.3 @@ -2,7 +2,8 @@
     1.4  %% $Id$
     1.5  
     1.6  %% toc
     1.7 -\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}}
     1.8 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     1.9 +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
    1.10  
    1.11  %% references
    1.12  \newcommand{\secref}[1]{\S\ref{#1}}
    1.13 @@ -11,10 +12,17 @@
    1.14  %% glossary
    1.15  \renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
    1.16  \newcommand{\seeglossary}[1]{\emph{#1}}
    1.17 -\def\glossaryname{Glossary}
    1.18 +\newcommand{\glossaryname}{Glossary}
    1.19  \renewcommand{\nomname}{\glossaryname}
    1.20  \renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
    1.21  
    1.22 +%% index
    1.23 +\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
    1.24 +\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    1.25 +\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    1.26 +\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    1.27 +
    1.28 +
    1.29  \newcommand{\drv}{\mathrel{\vdash}}
    1.30  \newcommand{\edrv}{\mathop{\drv}\nolimits}
    1.31  \newcommand{\Drv}[1]{\mathrel{\vdash_{#1}}}
    1.32 @@ -37,11 +45,6 @@
    1.33  \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
    1.34  \renewcommand{\endisatagmlref}{\endgroup}
    1.35  
    1.36 -\newcommand{\indexml}[1]{\index{\emph{#1} ({\ML})|bold}}
    1.37 -\newcommand{\indexmltype}[1]{\index{\emph{#1} ({\ML} type)|bold}}
    1.38 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} ({\ML} structure)|bold}}
    1.39 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} ({\ML} functor)|bold}}
    1.40 -
    1.41  \newcommand{\isasymTHEORY}{\isakeyword{theory}}
    1.42  \newcommand{\isasymIMPORTS}{\isakeyword{imports}}
    1.43  \newcommand{\isasymUSES}{\isakeyword{uses}}