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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
|
% =====================================================================
% HOL Manual LaTeX Source: finite_sets library (standard latex style)
% =====================================================================
\documentstyle[12pt,fleqn,
../../../Manual/LaTeX/alltt,
../../../Manual/LaTeX/layout]{book}
% ---------------------------------------------------------------------
% Input defined macros and commands
% ---------------------------------------------------------------------
\input{../../../Manual/LaTeX/commands}
\input{../../../Manual/LaTeX/ref-macros}
% ---------------------------------------------------------------------
% Define a few other commands.
% ---------------------------------------------------------------------
\def\bk{{\tt\char`\\}}
\def\lb{{\tt\char`\{}}
\def\rb{{\tt\char`\}}}
\def\vb{{\tt\char`\|}}
% --------------------------------------------------------------------- %
% Macro to make a nice underscore in the library name when typeset in %
% boldface. Standard \_ macro doesn't give tall enough underscore. %
% The underscore is used on the titlepage and in Chapter 1 title (hence %
% also on running heads) --- all in boldface. %
% --------------------------------------------------------------------- %
\def\und{\leavevmode%
\kern0.15ex \vbox{\hrule height0.1ex width0.3em}\kern0.2ex}
% ---------------------------------------------------------------------
% 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}
|
