1% =====================================================================
2% HOL Manual LaTeX Source: pair library (standard latex style)
3% =====================================================================
4
5\documentclass[12pt]{book}
6\usepackage{charter}
7\usepackage{fleqn}
8\usepackage{alltt}
9\usepackage{../../..//Manual/LaTeX/layout}
10\usepackage[T1]{fontenc}
11
12% ---------------------------------------------------------------------
13% Input defined macros and commands
14% ---------------------------------------------------------------------
15\input{../../../Manual/LaTeX/commands}
16\input{../../../Manual/LaTeX/ref-macros}
17
18% ---------------------------------------------------------------------
19% The document has an index
20% ---------------------------------------------------------------------
21\usepackage{makeidx}
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 \tableofcontents % table of contents
37
38   % ---------------------------------------------------------------------
39   % Systematic description of the library
40   % ---------------------------------------------------------------------
41
42   \pagenumbering{arabic} % arabic page numbers \setcounter{page}{1} %
43   start at page 1 \include{description}
44
45   % ---------------------------------------------------------------------
46   % Reference manual entries for functions
47   % ---------------------------------------------------------------------
48
49   \include{entries}
50
51   % ---------------------------------------------------------------------
52   % Listing of theorems
53   % ---------------------------------------------------------------------
54
55   \include{theorems}
56
57   % ---------------------------------------------------------------------
58   % Index
59   % ---------------------------------------------------------------------
60
61   {\def\_{{\char'137}}                  % \tt style `_' character
62
63     \printindex}
64
65 \end{document}
66