doc-src/IsarAdvanced/Codegen/style.sty
author haftmann
Tue Oct 10 12:08:12 2006 +0200 (2006-10-10)
changeset 20948 9b9910b82645
child 26781 861e06a047c5
permissions -rw-r--r--
initial draft
haftmann@20948
     1
haftmann@20948
     2
%% $Id$
haftmann@20948
     3
haftmann@20948
     4
%% toc
haftmann@20948
     5
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
haftmann@20948
     6
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
haftmann@20948
     7
haftmann@20948
     8
%% references
haftmann@20948
     9
\newcommand{\secref}[1]{\S\ref{#1}}
haftmann@20948
    10
\newcommand{\chref}[1]{chapter~\ref{#1}}
haftmann@20948
    11
\newcommand{\figref}[1]{figure~\ref{#1}}
haftmann@20948
    12
haftmann@20948
    13
%% glossary
haftmann@20948
    14
\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
haftmann@20948
    15
\newcommand{\seeglossary}[1]{\emph{#1}}
haftmann@20948
    16
\newcommand{\glossaryname}{Glossary}
haftmann@20948
    17
\renewcommand{\nomname}{\glossaryname}
haftmann@20948
    18
\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
haftmann@20948
    19
haftmann@20948
    20
%% index
haftmann@20948
    21
\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
haftmann@20948
    22
\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
haftmann@20948
    23
\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
haftmann@20948
    24
\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
haftmann@20948
    25
haftmann@20948
    26
%% math
haftmann@20948
    27
\newcommand{\text}[1]{\mbox{#1}}
haftmann@20948
    28
\newcommand{\isasymvartheta}{\isamath{\theta}}
haftmann@20948
    29
\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
haftmann@20948
    30
haftmann@20948
    31
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
haftmann@20948
    32
haftmann@20948
    33
\pagestyle{headings}
haftmann@20948
    34
\sloppy
haftmann@20948
    35
\binperiod
haftmann@20948
    36
\underscoreon
haftmann@20948
    37
haftmann@20948
    38
\renewcommand{\isadigit}[1]{\isamath{#1}}
haftmann@20948
    39
haftmann@20948
    40
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
haftmann@20948
    41
haftmann@20948
    42
\isafoldtag{FIXME}
haftmann@20948
    43
\isakeeptag{mlref}
haftmann@20948
    44
\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
haftmann@20948
    45
\renewcommand{\endisatagmlref}{\endgroup}
haftmann@20948
    46
haftmann@20948
    47
\newcommand{\isasymGUESS}{\isakeyword{guess}}
haftmann@20948
    48
\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
haftmann@20948
    49
\newcommand{\isasymTHEORY}{\isakeyword{theory}}
haftmann@20948
    50
\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
haftmann@20948
    51
\newcommand{\isasymUSES}{\isakeyword{uses}}
haftmann@20948
    52
\newcommand{\isasymBEGIN}{\isakeyword{begin}}
haftmann@20948
    53
\newcommand{\isasymEND}{\isakeyword{end}}
haftmann@20948
    54
\newcommand{\isasymCONSTS}{\isakeyword{consts}}
haftmann@20948
    55
\newcommand{\isasymDEFS}{\isakeyword{defs}}
haftmann@20948
    56
\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
haftmann@20948
    57
\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
haftmann@20948
    58
haftmann@20948
    59
\isabellestyle{it}
haftmann@20948
    60
haftmann@20948
    61
%%% Local Variables: 
haftmann@20948
    62
%%% mode: latex
haftmann@20948
    63
%%% TeX-master: "implementation"
haftmann@20948
    64
%%% End: