doc-src/IsarImplementation/style.sty
author wenzelm
Mon Jan 02 20:16:52 2006 +0100 (2006-01-02 ago)
changeset 18537 2681f9e34390
child 18554 bff7a1466fe4
permissions -rw-r--r--
"The Isabelle/Isar Implementation" manual;
     1 
     2 %% $Id$
     3 
     4 %% toc
     5 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}}
     6 
     7 %% references
     8 \newcommand{\secref}[1]{\S\ref{#1}}
     9 \newcommand{\figref}[1]{figure~\ref{#1}}
    10 
    11 %% glossary
    12 \renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
    13 \newcommand{\seeglossary}[1]{\emph{#1}}
    14 \def\glossaryname{Glossary}
    15 \renewcommand{\nomname}{\glossaryname}
    16 \renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
    17 
    18 \newcommand{\drv}{\mathrel{\vdash}}
    19 \newcommand{\edrv}{\mathop{\drv}\nolimits}
    20 \newcommand{\Drv}[1]{\mathrel{\vdash_{#1}}}
    21 \newcommand{\Or}{\mathrel{\;|\;}}
    22 
    23 \renewcommand{\vec}[1]{\overline{#1}}
    24 \renewcommand{\phi}{\varphi}
    25 
    26 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    27 
    28 \pagestyle{headings}
    29 \sloppy
    30 \binperiod
    31 \underscoreon
    32 
    33 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\medskip\endgroup}
    34 
    35 \isafoldtag{FIXME}
    36 \isakeeptag{mlref}
    37 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
    38 \renewcommand{\endisatagmlref}{\endgroup}
    39 
    40 \newcommand{\indexml}[1]{\index{\emph{#1} ({\ML})|bold}}
    41 \newcommand{\indexmltype}[1]{\index{\emph{#1} ({\ML} type)|bold}}
    42 \newcommand{\indexmlstructure}[1]{\index{\emph{#1} ({\ML} structure)|bold}}
    43 \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} ({\ML} functor)|bold}}
    44 
    45 \newcommand{\isasymTHEORY}{\isakeyword{theory}}
    46 \newcommand{\isasymIMPORTS}{\isakeyword{imports}}
    47 \newcommand{\isasymUSES}{\isakeyword{uses}}
    48 \newcommand{\isasymBEGIN}{\isakeyword{begin}}
    49 \newcommand{\isasymEND}{\isakeyword{end}}
    50 \newcommand{\isasymCONSTS}{\isakeyword{consts}}
    51 \newcommand{\isasymDEFS}{\isakeyword{defs}}
    52 \newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
    53 
    54 \isabellestyle{it}
    55 
    56 %%% Local Variables: 
    57 %%% mode: latex
    58 %%% TeX-master: "implementation"
    59 %%% End: