1% ===================================================================== 2% HOL Manual LaTeX Source: arith library (standard latex style) 3% ===================================================================== 4 5\documentclass[12pt]{book} 6 7\usepackage{fleqn} 8\usepackage{alltt} 9\usepackage{../../../../Manual/LaTeX/layout} 10\usepackage{makeidx} 11 12% --------------------------------------------------------------------- 13% Input defined macros and commands 14% --------------------------------------------------------------------- 15\input{../../../../Manual/LaTeX/commands} 16\input{../../../../Manual/LaTeX/ref-macros} 17\newcommand{\ptt}{\tt} 18 19% --------------------------------------------------------------------- 20% The document has an index 21% --------------------------------------------------------------------- 22\makeindex 23 24\begin{document} 25 26 \setlength{\unitlength}{1mm} % unit of length = 1mm 27 \setlength{\baselineskip}{16pt} % line spacing = 16pt 28 29 % --------------------------------------------------------------------- 30 % prelims 31 % --------------------------------------------------------------------- 32 33 \pagenumbering{roman} % roman page numbers for prelims 34 \setcounter{page}{1} % start at page 1 35 36 \include{title} % title page 37 \tableofcontents % table of contents 38 39 % --------------------------------------------------------------------- 40 % Systematic description of the library 41 % --------------------------------------------------------------------- 42 43 \cleardoublepage % kick to a right-hand page 44 \pagenumbering{arabic} % arabic page numbers 45 \setcounter{page}{1} % start at page 1 46 \include{description} 47 48 % --------------------------------------------------------------------- 49 % Reference manual entries for functions 50 % --------------------------------------------------------------------- 51 52 \include{entries} 53 54 % --------------------------------------------------------------------- 55 % References 56 % --------------------------------------------------------------------- 57 58 \include{references} 59 60 % --------------------------------------------------------------------- 61 % Index 62 % --------------------------------------------------------------------- 63 64 {\def\_{{\char'137}} % \tt style `_' character 65 66 \printindex} 67 68\end{document} 69 70 71