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