1% =====================================================================
2% HOL Manual LaTeX Source: pred_sets library (standard latex style)
3% =====================================================================
4
5\documentclass[12pt]{book}
6
7\usepackage{fleqn}
8\usepackage{alltt}
9\usepackage{charter}
10\usepackage{makeidx}
11\usepackage{../../../Manual/LaTeX/layout}
12
13% ---------------------------------------------------------------------
14% Input defined macros and commands
15% ---------------------------------------------------------------------
16\input{../../../Manual/LaTeX/commands}
17\input{../../../Manual/LaTeX/ref-macros}
18\def\ptt{\tt}
19
20% ---------------------------------------------------------------------
21% Define a few other commands.
22% ---------------------------------------------------------------------
23\def\bk{{\tt\char`\\}}
24\def\lb{{\tt\char`\{}}
25\def\rb{{\tt\char`\}}}
26\def\vb{{\tt\char`\|}}
27
28% --------------------------------------------------------------------- %
29% Macro to make a nice underscore in the library name when typeset in   %
30% boldface.  Standard \_ macro doesn't give tall enough underscore.     %
31% The underscore is used on the titlepage and in Chapter 1 title (hence %
32% also on running heads) --- all in boldface.                           %
33% --------------------------------------------------------------------- %
34
35\def\und{\leavevmode%
36\kern0.15ex \vbox{\hrule height0.1ex width0.3em}\kern0.2ex}
37
38% ---------------------------------------------------------------------
39% The document has an index
40% ---------------------------------------------------------------------
41\makeindex
42
43\begin{document}
44
45   \setlength{\unitlength}{1mm}           % unit of length = 1mm
46   \setlength{\baselineskip}{16pt}        % line spacing = 16pt
47
48   % ---------------------------------------------------------------------
49   % prelims
50   % ---------------------------------------------------------------------
51
52   \pagenumbering{roman}                  % roman page numbers for prelims
53   \setcounter{page}{1}                   % start at page 1
54
55   \include{title}                        % title page
56   \tableofcontents                       % table of contents
57
58   % ---------------------------------------------------------------------
59   % Systematic description of the library
60   % ---------------------------------------------------------------------
61
62   \cleardoublepage                      % kick to a right-hand page
63   \pagenumbering{arabic}                % arabic page numbers
64   \setcounter{page}{1}                  % start at page 1
65   \include{description}
66
67   % ---------------------------------------------------------------------
68   % Reference manual entries for functions
69   % ---------------------------------------------------------------------
70
71   \include{entries}
72
73   % ---------------------------------------------------------------------
74   % Listing of theorems
75   % ---------------------------------------------------------------------
76
77   \include{theorems}
78
79   % ---------------------------------------------------------------------
80   % References
81   % ---------------------------------------------------------------------
82
83   \include{references}
84
85   % ---------------------------------------------------------------------
86   % Index
87   % ---------------------------------------------------------------------
88
89   {\def\_{{\char'137}}                  % \tt style `_' character
90
91    \printindex }
92%    \include{index}}
93
94\end{document}
95
96
97