uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
more robust handling of "|" within index;
3 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
4 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
7 \newcommand{\secref}[1]{\S\ref{#1}}
10 \newcommand{\strong}[1]{{\bfseries {#1}}}
11 \newcommand{\qn}[1]{\emph{#1}}
13 %% typographic conventions
14 \newcommand{\qt}[1]{``{#1}''}
17 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
22 \newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
23 \renewcommand{\isatagquote}{\begin{quotesegment}}
24 \renewcommand{\endisatagquote}{\end{quotesegment}}
28 \renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
29 \renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
32 \newcommand{\isasymSML}{SML}
35 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
41 \renewcommand{\isadigit}[1]{\isamath{#1}}
44 \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
47 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
48 \renewcommand{\endisatagmlref}{\endgroup}
55 %%% TeX-master: "implementation"