1% =====================================================================
2% HOL Manual LaTeX Source: arith library (standard latex style)
3% =====================================================================
4
5\documentclass[12pt]{book}
6
7\usepackage{fleqn}
8\usepackage{alltt}
9\usepackage{../../../../Manual/LaTeX/layout}
10\usepackage{makeidx}
11
12% ---------------------------------------------------------------------
13% Input defined macros and commands
14% ---------------------------------------------------------------------
15\input{../../../../Manual/LaTeX/commands}
16\input{../../../../Manual/LaTeX/ref-macros}
17\newcommand{\ptt}{\tt}
18
19% ---------------------------------------------------------------------
20% The document has an index
21% ---------------------------------------------------------------------
22\makeindex
23
24\begin{document}
25
26   \setlength{\unitlength}{1mm}           % unit of length = 1mm
27   \setlength{\baselineskip}{16pt}        % line spacing = 16pt
28
29   % ---------------------------------------------------------------------
30   % prelims
31   % ---------------------------------------------------------------------
32
33   \pagenumbering{roman}                  % roman page numbers for prelims
34   \setcounter{page}{1}                   % start at page 1
35
36   \include{title}                        % title page
37   \tableofcontents                       % table of contents
38
39   % ---------------------------------------------------------------------
40   % Systematic description of the library
41   % ---------------------------------------------------------------------
42
43   \cleardoublepage                      % kick to a right-hand page
44   \pagenumbering{arabic}                % arabic page numbers
45   \setcounter{page}{1}                  % start at page 1
46   \include{description}
47
48   % ---------------------------------------------------------------------
49   % Reference manual entries for functions
50   % ---------------------------------------------------------------------
51
52   \include{entries}
53
54   % ---------------------------------------------------------------------
55   % References
56   % ---------------------------------------------------------------------
57
58   \include{references}
59
60   % ---------------------------------------------------------------------
61   % Index
62   % ---------------------------------------------------------------------
63
64   {\def\_{{\char'137}}                  % \tt style `_' character
65
66    \printindex}
67
68\end{document}
69
70
71