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