% =====================================================================
% HOL Manual LaTeX Source: res_quan library (standard latex style)
% =====================================================================

\documentstyle[12pt,fleqn,makeidx,
               ../../../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`\|}}

\def\resquan{{\tt res\_quan}}
\def\THM{\relax\ifmmode\vdash\else$\vdash$\fi}
\def\AND{\relax\ifmmode\wedge\else$\wedge$\fi}
\def\OR{\relax\ifmmode\vee\else$\vee$\fi}
\def\IMP{\relax\ifmmode\supset\else$\supset$\fi}
\def\DOT{\relax\ifmmode.\,\else$.\,$\fi}

% ---------------------------------------------------------------------
% 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}

   % ---------------------------------------------------------------------
   % Index
   % ---------------------------------------------------------------------
 
   {\def\_{{\char'137}}		         % \tt style `_' character

    \printindex}

\end{document}


