1 |
|
2 %% $Id$ |
|
3 |
1 |
4 %% toc |
2 %% toc |
5 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} |
3 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} |
6 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} |
4 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} |
7 |
5 |
8 %% references |
6 %% references |
9 \newcommand{\secref}[1]{\S\ref{#1}} |
7 \newcommand{\secref}[1]{\S\ref{#1}} |
10 \newcommand{\chref}[1]{chapter~\ref{#1}} |
|
11 \newcommand{\figref}[1]{figure~\ref{#1}} |
8 \newcommand{\figref}[1]{figure~\ref{#1}} |
12 |
9 |
13 %% glossary |
10 %% logical markup |
14 \renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}} |
11 \newcommand{\strong}[1]{{\bfseries {#1}}} |
15 \newcommand{\seeglossary}[1]{\emph{#1}} |
12 \newcommand{\qn}[1]{\emph{#1}} |
16 \newcommand{\glossaryname}{Glossary} |
|
17 \renewcommand{\nomname}{\glossaryname} |
|
18 \renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}} |
|
19 |
13 |
20 %% index |
14 %% typographic conventions |
21 \newcommand{\indexml}[1]{\index{\emph{#1}|bold}} |
15 \newcommand{\qt}[1]{``{#1}''} |
22 \newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}} |
|
23 \newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}} |
|
24 \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}} |
|
25 |
16 |
26 %% math |
17 %% verbatim text |
27 \newcommand{\text}[1]{\mbox{#1}} |
18 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} |
28 \newcommand{\isasymvartheta}{\isamath{\theta}} |
|
29 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}} |
|
30 |
19 |
|
20 %% quoted segments |
|
21 \makeatletter |
|
22 \isakeeptag{quote} |
|
23 \newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}} |
|
24 \renewcommand{\isatagquote}{\begin{quotesegment}} |
|
25 \renewcommand{\endisatagquote}{\end{quotesegment}} |
|
26 \makeatother |
|
27 |
|
28 %% presentation |
31 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
29 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
32 |
30 |
33 \pagestyle{headings} |
31 \pagestyle{headings} |
34 \sloppy |
|
35 \binperiod |
32 \binperiod |
36 \underscoreon |
33 \underscoreon |
37 |
34 |
38 \renewcommand{\isadigit}[1]{\isamath{#1}} |
35 \renewcommand{\isadigit}[1]{\isamath{#1}} |
39 |
36 |
40 \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup} |
37 \isabellestyle{it} |
41 |
38 |
42 \isafoldtag{FIXME} |
|
43 \isakeeptag{mlref} |
|
44 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small} |
|
45 \renewcommand{\endisatagmlref}{\endgroup} |
|
46 |
|
47 \newcommand{\isasymGUESS}{\isakeyword{guess}} |
|
48 \newcommand{\isasymOBTAIN}{\isakeyword{obtain}} |
|
49 \newcommand{\isasymTHEORY}{\isakeyword{theory}} |
|
50 \newcommand{\isasymUSES}{\isakeyword{uses}} |
|
51 \newcommand{\isasymEND}{\isakeyword{end}} |
|
52 \newcommand{\isasymCONSTS}{\isakeyword{consts}} |
|
53 \newcommand{\isasymDEFS}{\isakeyword{defs}} |
|
54 \newcommand{\isasymTHEOREM}{\isakeyword{theorem}} |
|
55 \newcommand{\isasymDEFINITION}{\isakeyword{definition}} |
|
56 |
|
57 \isabellestyle{it} |
|
58 |
39 |
59 %%% Local Variables: |
40 %%% Local Variables: |
60 %%% mode: latex |
41 %%% mode: latex |
61 %%% TeX-master: "implementation" |
42 %%% TeX-master: "implementation" |
62 %%% End: |
43 %%% End: |