|
1 %% toc |
|
2 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} |
|
3 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} |
|
4 |
|
5 %% references |
|
6 \newcommand{\secref}[1]{\S\ref{#1}} |
|
7 \newcommand{\chref}[1]{chapter~\ref{#1}} |
|
8 \newcommand{\figref}[1]{figure~\ref{#1}} |
|
9 |
|
10 %% math |
|
11 \newcommand{\text}[1]{\mbox{#1}} |
|
12 \newcommand{\isasymvartheta}{\isamath{\theta}} |
|
13 \newcommand{\isactrlvec}[1]{\emph{$\vec{#1}$}} |
|
14 \newcommand{\isactrlBG}{\isacharbackquoteopen} |
|
15 \newcommand{\isactrlEN}{\isacharbackquoteclose} |
|
16 |
|
17 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
|
18 |
|
19 \pagestyle{headings} |
|
20 \sloppy |
|
21 \binperiod |
|
22 |
|
23 \parindent 0pt\parskip 0.5ex |
|
24 |
|
25 \renewcommand{\isadigit}[1]{\isamath{#1}} |
|
26 |
|
27 \renewcommand{\isaantiqopen}{\isasymlbrace} |
|
28 \renewcommand{\isaantiqclose}{\isasymrbrace} |
|
29 |
|
30 \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup} |
|
31 |
|
32 \isafoldtag{FIXME} |
|
33 |
|
34 \isakeeptag{mlref} |
|
35 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}} |
|
36 \renewcommand{\endisatagmlref}{} |
|
37 |
|
38 \isakeeptag{mlantiq} |
|
39 \renewcommand{\isatagmlantiq}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Antiquotations}} |
|
40 \renewcommand{\endisatagmlantiq}{} |
|
41 |
|
42 \isakeeptag{mlex} |
|
43 \renewcommand{\isatagmlex}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Examples}} |
|
44 \renewcommand{\endisatagmlex}{} |
|
45 |
|
46 \renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}} |
|
47 \renewcommand{\endisatagML}{\endgroup} |
|
48 |
|
49 \newcommand{\minorcmd}[1]{{\sf #1}} |
|
50 \newcommand{\isasymtype}{\minorcmd{type}} |
|
51 \newcommand{\isasymval}{\minorcmd{val}} |
|
52 |
|
53 \newcommand{\isasymFIX}{\isakeyword{fix}} |
|
54 \newcommand{\isasymASSUME}{\isakeyword{assume}} |
|
55 \newcommand{\isasymDEFINE}{\isakeyword{define}} |
|
56 \newcommand{\isasymNOTE}{\isakeyword{note}} |
|
57 \newcommand{\isasymGUESS}{\isakeyword{guess}} |
|
58 \newcommand{\isasymOBTAIN}{\isakeyword{obtain}} |
|
59 \newcommand{\isasymTHEORY}{\isakeyword{theory}} |
|
60 \newcommand{\isasymUSES}{\isakeyword{uses}} |
|
61 \newcommand{\isasymEND}{\isakeyword{end}} |
|
62 \newcommand{\isasymCONSTS}{\isakeyword{consts}} |
|
63 \newcommand{\isasymDEFS}{\isakeyword{defs}} |
|
64 \newcommand{\isasymTHEOREM}{\isakeyword{theorem}} |
|
65 \newcommand{\isasymDEFINITION}{\isakeyword{definition}} |
|
66 |
|
67 \isabellestyle{literal} |
|
68 |
|
69 \railtermfont{\isabellestyle{tt}} |
|
70 \railnontermfont{\isabellestyle{itunderscore}} |
|
71 \railnamefont{\isabellestyle{itunderscore}} |