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