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