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