|
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: |