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