1% =====================================================================
2% HOL Manual LaTeX Source: reduce library (standard latex style)
3% =====================================================================
4
5\documentclass[12pt]{book}
6
7\usepackage{fleqn}
8\usepackage{makeidx}
9\usepackage{alltt}
10\usepackage{../../../../Manual/LaTeX/layout}
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\makeindex
22
23\begin{document}
24
25   \setlength{\unitlength}{1mm}           % unit of length = 1mm
26   \setlength{\baselineskip}{16pt}        % line spacing = 16pt
27
28   % ---------------------------------------------------------------------
29   % prelims
30   % ---------------------------------------------------------------------
31
32   \pagenumbering{roman}                  % roman page numbers for prelims
33   \setcounter{page}{1}                   % start at page 1
34
35   \include{title}                        % title page
36   \tableofcontents                       % table of contents
37
38   % ---------------------------------------------------------------------
39   % Systematic description of the library
40   % ---------------------------------------------------------------------
41
42   \cleardoublepage			 % kick to a right-hand page
43   \pagenumbering{arabic}                % arabic page numbers
44   \setcounter{page}{1}                  % start at page 1
45   \include{description}
46
47   % ---------------------------------------------------------------------
48   % Reference manual entries for functions
49   % ---------------------------------------------------------------------
50
51   \include{entries}
52
53   % ---------------------------------------------------------------------
54   % Index
55   % ---------------------------------------------------------------------
56
57   {\def\_{{\char'137}}                  % \tt style `_' character
58
59    \printindex }
60%    \include{index}}
61
62\end{document}
63