1% =====================================================================
2% HOL Manual LaTeX Source: res_quan library (standard latex style)
3% =====================================================================
4
5\documentclass[12pt]{book}
6\usepackage{fleqn}
7\usepackage{makeidx}
8\usepackage{alltt}
9\usepackage{fancyvrb}
10\usepackage{../../../Manual/LaTeX/layout}
11\usepackage{charter}
12
13% ---------------------------------------------------------------------
14% Input defined macros and commands
15% ---------------------------------------------------------------------
16\input{../../../Manual/LaTeX/commands}
17\input{../../../Manual/LaTeX/ref-macros}
18
19% ---------------------------------------------------------------------
20% Define a few other commands.
21% ---------------------------------------------------------------------
22\def\bk{{\tt\char`\\}}
23\def\lb{{\tt\char`\{}}
24\def\rb{{\tt\char`\}}}
25\def\vb{{\tt\char`\|}}
26
27\def\resquan{{\tt res\_quan}}
28\def\THM{\relax\ifmmode\vdash\else$\vdash$\fi}
29\def\AND{\relax\ifmmode\wedge\else$\wedge$\fi}
30\def\OR{\relax\ifmmode\vee\else$\vee$\fi}
31\def\IMP{\relax\ifmmode\supset\else$\supset$\fi}
32\def\DOT{\relax\ifmmode.\,\else$.\,$\fi}
33
34% ---------------------------------------------------------------------
35% The document has an index
36% ---------------------------------------------------------------------
37\makeindex
38
39\begin{document}
40
41   \setlength{\unitlength}{1mm}           % unit of length = 1mm
42   \setlength{\baselineskip}{16pt}        % line spacing = 16pt
43
44   % ---------------------------------------------------------------------
45   % prelims
46   % ---------------------------------------------------------------------
47
48   \pagenumbering{roman}                  % roman page numbers for prelims
49   \setcounter{page}{1}                   % start at page 1
50
51   \include{title}                        % title page
52   \tableofcontents                       % table of contents
53
54   % ---------------------------------------------------------------------
55   % Systematic description of the library
56   % ---------------------------------------------------------------------
57
58   \cleardoublepage                      % kick to a right-hand page
59   \pagenumbering{arabic}                % arabic page numbers
60   \setcounter{page}{1}                  % start at page 1
61   \include{description}
62
63   % ---------------------------------------------------------------------
64   % Reference manual entries for functions
65   % ---------------------------------------------------------------------
66
67   \include{entries}
68
69   % ---------------------------------------------------------------------
70   % Listing of theorems
71   % ---------------------------------------------------------------------
72
73%   \include{theorems}
74
75   % ---------------------------------------------------------------------
76   % Index
77   % ---------------------------------------------------------------------
78
79   {\def\_{{\char'137}}                  % \tt style `_' character
80
81    \printindex}
82
83\end{document}
84
85
86