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