1% ===================================================================== 2% 3% LaTeX style file for the HOL system manual 4% 5% ===================================================================== 6 7% --------------------------------------------------------------------- 8% BOOLEAN FLAG FOR PAPER SIZE. 9% 10% set: \Afourtrue to make paper size A4 11% \Afourfalse to make paper size 8.5 x 11 inches 12% --------------------------------------------------------------------- 13 14\newif\ifAfour 15\Afourtrue 16 17% --------------------------------------------------------------------- 18% PAPER SIZE (latex overrides these anyway) 19% 20% TeX expects 1 inch margins all around. 21% * a4 (european paper) is exactly 297mm high by 210mm wide 22% * 8.5x11 (american paper) is exactly 279.4mm high by 215.9mm wide 23% 24% 1 inch = 25.4 mm 25% --------------------------------------------------------------------- 26 27\ifAfour 28 \usepackage[a4paper,width=160truemm,height=225truemm,top=38mm, 29 headheight=16pt,headsep=20pt,footskip=13mm]{geometry} 30\else 31 \usepackage[letterpaper,width=160truemm,height=225truemm,top=32mm, 32 headheight=16pt,headsep=20pt,footskip=13mm]{geometry} 33\fi 34 35% --------------------------------------------------------------------- 36% FONT 37% --------------------------------------------------------------------- 38 39\usepackage{stix} 40\renewcommand{\rmdefault}{bch} 41\def\@pnumwidth{8mm} 42 43\usepackage{microtype} 44\DisableLigatures{encoding = T1, family = tt*} 45 46% --------------------------------------------------------------------- 47% MATH INDENTATION. = \tabcolsep + three small verbatim spaces (!) 48% --------------------------------------------------------------------- 49%\setlength{\mathindent}{\tabcolsep} 50%\addtolength{\mathindent}{\the\fontdimen2\elvtt} 51%\addtolength{\mathindent}{\the\fontdimen2\elvtt} 52%\addtolength{\mathindent}{\the\fontdimen2\elvtt} 53 54\setlength{\mathindent}{\tabcolsep} 55\newbox\temp 56\setbox\temp=\hbox{\small\verb! !} 57\addtolength{\mathindent}{\wd\temp} 58 59% --------------------------------------------------------------------- 60% INDENTATION: 4mm indentation 61% --------------------------------------------------------------------- 62\parindent 4mm 63 64% --------------------------------------------------------------------- 65% FOOTNOTES: footnotes are in 10 point font. 66% 67% put 12+1-1 points between text and rule 68% put 10pt between at start of footnote 69% foot note rule is 40mm long 70% --------------------------------------------------------------------- 71\skip\footins 12pt plus 2pt minus 2pt 72\footnotesep 10pt 73\def\footnoterule{\kern-3\p@ \hrule width 40mm \kern 2.6\p@} 74 75% --------------------------------------------------------------------- 76% FLOATS 77% --------------------------------------------------------------------- 78\floatsep 12pt plus 2pt minus 2pt 79\textfloatsep 20pt plus 2pt minus 4pt 80\intextsep 12pt plus 2pt minus 2pt 81%\@maxsep 20pt 82 83% --------------------------------------------------------------------- 84% Make "@" a "letter" for definitions that follow 85% --------------------------------------------------------------------- 86\makeatletter 87 88% --------------------------------------------------------------------- 89% CHAPTER HEADINGS (deriving from Larry Paulson) 90% --------------------------------------------------------------------- 91 92\def\@rulehead#1{\hrule height1pt \vskip 14pt \huge \bf 93 #1 \vskip 14pt\hrule height1pt} 94 95\def\@makechapterhead#1{ { \parindent 0pt 96\ifnum \c@secnumdepth >\m@ne \raggedright\large\bf \@chapapp{} \thechapter\par 97 \vskip 8pt \fi \raggedright \@rulehead{#1} \par 98 \nobreak \vskip 50pt } } 99 100\def\@makeschapterhead#1{ { \parindent 0pt {\large\bf\phantom{Chapter}} \par 101 \vskip 8pt \raggedright 102 \@rulehead{#1} \par \nobreak \vskip 50pt } } 103 104 105% --------------------------------------------------------------------- 106% PAGE FOOT, on pages that start a new chapter 107% --------------------------------------------------------------------- 108 109\def\ps@plain{\let\@mkboth\@gobbletwo 110 \def\@oddhead{}\def\@oddfoot{\rm\bf\hfil\thepage 111 \hfil}\def\@evenhead{}\let\@evenfoot\@oddfoot} 112 113% --------------------------------------------------------------------- 114% PAGE HEADINGS 115% --------------------------------------------------------------------- 116 117\def\ps@headings{\def\@oddfoot{}\def\@evenfoot{}\def 118 \@evenhead{\vbox{\hbox to \textwidth{\bf\thepage\hfil\bf\leftmark 119 }\vskip-\prevdepth\vskip 4.5pt\hrule height0.9pt}}\def 120 \@oddhead{\vbox{\hbox to \textwidth{\bf\rightmark\hfil\bf 121 \thepage}\vskip-\prevdepth\vskip 4.5pt\hrule height0.9pt}}\def 122 \chaptermark##1{\markboth {{\ifnum \c@secnumdepth 123>\m@ne 124\@chapapp\ \thechapter. \ \fi ##1}}{}}\def\sectionmark##1{\markright 125{{\ifnum \c@secnumdepth >\z@ 126\thesection. \ \fi ##1}}}} 127 128% --------------------------------------------------------------------- 129% Part 130% --------------------------------------------------------------------- 131\def\part{\cleardoublepage \thispagestyle{empty} \if@twocolumn \onecolumn 132\@tempswatrue \else \@tempswafalse \fi \hbox{}\vfil \bgroup \centering 133\secdef\@part\@spart} 134 135\def\@endpart{\par\egroup \vfil\newpage \if@twoside \hbox{} 136\thispagestyle{empty} 137 \newpage 138 \fi \if@tempswa \twocolumn \fi} 139 140% --------------------------------------------------------------------- 141% REFERENCES 142% 143% (1) For references in each volume use: 144% 145% \begin{thebibliography} ... \end{thebibliography} 146% 147% This makes the references a new chapter. 148% 149% (2) For case study references, also use: 150% 151% \begin{thebibliography} ... \end{thebibliography} 152% 153% This makes the references in a case study an unumbered section. 154% 155% NOTE: references in case studies should have different names than 156% those in the body of the tutorial. (I.e. different \bibitem name). 157% --------------------------------------------------------------------- 158 159\def\bibname{References} 160 161% --------------------------------------------------------------------- 162% Enumeration with Roman numerals: one-level enumeration only 163% --------------------------------------------------------------------- 164 165\newcount\@myenumdepth \@myenumdepth = 0 166\@definecounter{myenumi} 167 168%\newenvironment{myenumerate}{\begin{enumerate}}{\end{enumerate}} 169% \renewcommand{\theenumi}{\roman{enumi}} 170% \renewcommand{\labelenumi}{(\roman{enumi})}}{\end{enumerate}} 171 172\def\myenumerate{\ifnum \@myenumdepth >0 \@toodeep\else 173 \advance\@myenumdepth \@ne 174 \list{(\roman{myenumi})}{\usecounter{myenumi} 175 \settowidth{\labelwidth}{(iii)} 176 \setlength{\leftmargin}{\labelwidth} 177 \addtolength{\leftmargin}{\labelsep} 178 \addtolength{\leftmargin}{\mathindent} 179 \def\makelabel##1{\hss\llap{##1}}}\fi} 180 181\let\endmyenumerate =\endlist 182 183 184% --------------------------------------------------------------------- 185% Enumerate envoronment for proofs in drules.tex 186% --------------------------------------------------------------------- 187 188\def\proof{\ifnum \@enumdepth >0 \@toodeep\else 189 \advance\@enumdepth \@ne 190 \edef\@enumctr{enum\romannumeral\the\@enumdepth}\list 191 {\csname label\@enumctr\endcsname}{\usecounter 192 {\@enumctr}\setlength{\itemsep}{0.0mm} 193 \setlength{\baselineskip}{13pt} 194 \def\makelabel##1{\hss\llap{##1}}}\fi} 195 196\let\endproof =\endlist 197 198% --------------------------------------------------------------------- 199% Make "@" an "other" again 200% --------------------------------------------------------------------- 201\makeatother 202 203 204 205% --------------------------------------------------------------------- 206% Preliminary settings etc. 207% --------------------------------------------------------------------- 208 209\renewcommand{\topfraction}{0.8} % 0.8 of the top page can be fig. 210\renewcommand{\bottomfraction}{0.8} % 0.8 of the bottom page can be fig. 211\renewcommand{\textfraction}{0.1} % 0.1 of the page must contain text 212\setcounter{totalnumber}{4} % max of 4 figures per page 213\setcounter{secnumdepth}{3} % number sections down to level 3 214\setcounter{tocdepth}{2} % toc contains numbers to level 2 215\flushbottom % text extends right to the bottom 216