% =====================================================================
%
% LaTeX style file for the HOL system manual
%
% =====================================================================

% ---------------------------------------------------------------------
% BOOLEAN FLAG FOR PAPER SIZE.
%
% set:   \Afourtrue    to make paper size A4
%        \Afourfalse   to make paper size 8.5 x 11 inches
% ---------------------------------------------------------------------

\newif\ifAfour
\Afourtrue

% ---------------------------------------------------------------------
% PAPER SIZE  (latex overrides these anyway)
%
% TeX expects 1 inch margins all around.
%    * a4 (european paper) is exactly 297mm high by 210mm wide
%    * 8.5x11 (american paper) is exactly 279.4mm high by 215.9mm wide
%
% 1 inch = 25.4 mm
% ---------------------------------------------------------------------

\ifAfour
  \usepackage[a4paper,width=160truemm,height=225truemm,top=38mm,
              headheight=16pt,headsep=20pt,footskip=13mm]{geometry}
\else
  \usepackage[letterpaper,width=160truemm,height=225truemm,top=32mm,
              headheight=16pt,headsep=20pt,footskip=13mm]{geometry}
\fi

% ---------------------------------------------------------------------
% FONT
% ---------------------------------------------------------------------

\usepackage{stix}
\renewcommand{\rmdefault}{bch}
\def\@pnumwidth{8mm}

\usepackage{microtype}
\DisableLigatures{encoding = T1, family = tt*}

% ---------------------------------------------------------------------
% MATH INDENTATION.  = \tabcolsep + three small verbatim spaces  (!)
% ---------------------------------------------------------------------
%\setlength{\mathindent}{\tabcolsep}
%\addtolength{\mathindent}{\the\fontdimen2\elvtt}
%\addtolength{\mathindent}{\the\fontdimen2\elvtt}
%\addtolength{\mathindent}{\the\fontdimen2\elvtt}

\setlength{\mathindent}{\tabcolsep}
\newbox\temp
\setbox\temp=\hbox{\small\verb!   !}
\addtolength{\mathindent}{\wd\temp}

% ---------------------------------------------------------------------
% INDENTATION: 4mm indentation
% ---------------------------------------------------------------------
\parindent 4mm

% ---------------------------------------------------------------------
% FOOTNOTES: footnotes are in 10 point font.
%
% put 12+1-1 points between text and rule
% put 10pt between at start of footnote
% foot note rule is 40mm long
% ---------------------------------------------------------------------
\skip\footins 12pt plus 2pt minus 2pt
\footnotesep 10pt
\def\footnoterule{\kern-3\p@ \hrule width 40mm \kern 2.6\p@}

% ---------------------------------------------------------------------
% FLOATS
% ---------------------------------------------------------------------
\floatsep 12pt plus 2pt minus 2pt
\textfloatsep  20pt plus 2pt minus 4pt
\intextsep 12pt plus 2pt minus 2pt
%\@maxsep 20pt

% ---------------------------------------------------------------------
% Make "@" a "letter" for definitions that follow
% ---------------------------------------------------------------------
\makeatletter

% ---------------------------------------------------------------------
% CHAPTER HEADINGS (deriving from Larry Paulson)
% ---------------------------------------------------------------------

\def\@rulehead#1{\hrule height1pt \vskip 14pt \huge \bf
   #1 \vskip 14pt\hrule height1pt}

\def\@makechapterhead#1{ { \parindent 0pt
\ifnum \c@secnumdepth >\m@ne \raggedright\large\bf \@chapapp{} \thechapter\par
 \vskip 8pt \fi \raggedright \@rulehead{#1} \par
 \nobreak \vskip 50pt } }

\def\@makeschapterhead#1{ { \parindent 0pt {\large\bf\phantom{Chapter}} \par
   \vskip 8pt \raggedright
 \@rulehead{#1} \par \nobreak \vskip 50pt } }


% ---------------------------------------------------------------------
% PAGE FOOT, on pages that start a new chapter
% ---------------------------------------------------------------------

\def\ps@plain{\let\@mkboth\@gobbletwo
     \def\@oddhead{}\def\@oddfoot{\rm\bf\hfil\thepage
     \hfil}\def\@evenhead{}\let\@evenfoot\@oddfoot}

% ---------------------------------------------------------------------
% PAGE HEADINGS
% ---------------------------------------------------------------------

\def\ps@headings{\def\@oddfoot{}\def\@evenfoot{}\def
  \@evenhead{\vbox{\hbox to \textwidth{\bf\thepage\hfil\bf\leftmark
        }\vskip-\prevdepth\vskip 4.5pt\hrule height0.9pt}}\def
  \@oddhead{\vbox{\hbox to \textwidth{\bf\rightmark\hfil\bf
        \thepage}\vskip-\prevdepth\vskip 4.5pt\hrule height0.9pt}}\def
  \chaptermark##1{\markboth {{\ifnum \c@secnumdepth
>\m@ne
\@chapapp\ \thechapter. \ \fi ##1}}{}}\def\sectionmark##1{\markright
{{\ifnum \c@secnumdepth >\z@
\thesection. \ \fi ##1}}}}

% ---------------------------------------------------------------------
% Part
% ---------------------------------------------------------------------
\def\part{\cleardoublepage \thispagestyle{empty} \if@twocolumn \onecolumn
\@tempswatrue \else \@tempswafalse \fi \hbox{}\vfil \bgroup \centering
\secdef\@part\@spart}

\def\@endpart{\par\egroup \vfil\newpage \if@twoside \hbox{}
\thispagestyle{empty}
 \newpage
 \fi \if@tempswa \twocolumn \fi}

% ---------------------------------------------------------------------
% REFERENCES
%
% (1) For references in each volume use:
%
%        \begin{thebibliography} ... \end{thebibliography}
%
%     This makes the references a new chapter.
%
% (2) For case study references, also use:
%
%        \begin{thebibliography} ... \end{thebibliography}
%
%     This makes the references in a case study an unumbered section.
%
% NOTE: references in case studies should have different names than
%       those in the body of the tutorial.  (I.e. different \bibitem name).
% ---------------------------------------------------------------------

\def\bibname{References}

% ---------------------------------------------------------------------
% Enumeration with Roman numerals: one-level enumeration only
% ---------------------------------------------------------------------

\newcount\@myenumdepth \@myenumdepth = 0
\@definecounter{myenumi}

%\newenvironment{myenumerate}{\begin{enumerate}}{\end{enumerate}}
%  \renewcommand{\theenumi}{\roman{enumi}}
%  \renewcommand{\labelenumi}{(\roman{enumi})}}{\end{enumerate}}

\def\myenumerate{\ifnum \@myenumdepth >0 \@toodeep\else
      \advance\@myenumdepth \@ne
       \list{(\roman{myenumi})}{\usecounter{myenumi}
            \settowidth{\labelwidth}{(iii)}
            \setlength{\leftmargin}{\labelwidth}
            \addtolength{\leftmargin}{\labelsep}
            \addtolength{\leftmargin}{\mathindent}
            \def\makelabel##1{\hss\llap{##1}}}\fi}

\let\endmyenumerate =\endlist


% ---------------------------------------------------------------------
% Enumerate envoronment for proofs in drules.tex
% ---------------------------------------------------------------------

\def\proof{\ifnum \@enumdepth >0 \@toodeep\else
      \advance\@enumdepth \@ne
      \edef\@enumctr{enum\romannumeral\the\@enumdepth}\list
      {\csname label\@enumctr\endcsname}{\usecounter
        {\@enumctr}\setlength{\itemsep}{0.0mm}
        \setlength{\baselineskip}{13pt}
        \def\makelabel##1{\hss\llap{##1}}}\fi}

\let\endproof =\endlist

% ---------------------------------------------------------------------
% Make "@" an "other" again
% ---------------------------------------------------------------------
\makeatother



% ---------------------------------------------------------------------
% Preliminary settings etc.
% ---------------------------------------------------------------------

\renewcommand{\topfraction}{0.8}          % 0.8 of the top page can be fig.
\renewcommand{\bottomfraction}{0.8}       % 0.8 of the bottom page can be fig.
\renewcommand{\textfraction}{0.1}         % 0.1 of the page must contain text
\setcounter{totalnumber}{4}               % max of 4 figures per page
\setcounter{secnumdepth}{3}               % number sections down to level 3
\setcounter{tocdepth}{2}                  % toc contains numbers to level 2
\flushbottom                              % text extends right to the bottom