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