1% ===================================================================== 2% HOL Manual LaTeX Source: pred_sets library (standard latex style) 3% ===================================================================== 4 5\documentclass[12pt]{book} 6 7\usepackage{fleqn} 8\usepackage{alltt} 9\usepackage{charter} 10\usepackage{makeidx} 11\usepackage{../../../Manual/LaTeX/layout} 12 13% --------------------------------------------------------------------- 14% Input defined macros and commands 15% --------------------------------------------------------------------- 16\input{../../../Manual/LaTeX/commands} 17\input{../../../Manual/LaTeX/ref-macros} 18\def\ptt{\tt} 19 20% --------------------------------------------------------------------- 21% Define a few other commands. 22% --------------------------------------------------------------------- 23\def\bk{{\tt\char`\\}} 24\def\lb{{\tt\char`\{}} 25\def\rb{{\tt\char`\}}} 26\def\vb{{\tt\char`\|}} 27 28% --------------------------------------------------------------------- % 29% Macro to make a nice underscore in the library name when typeset in % 30% boldface. Standard \_ macro doesn't give tall enough underscore. % 31% The underscore is used on the titlepage and in Chapter 1 title (hence % 32% also on running heads) --- all in boldface. % 33% --------------------------------------------------------------------- % 34 35\def\und{\leavevmode% 36\kern0.15ex \vbox{\hrule height0.1ex width0.3em}\kern0.2ex} 37 38% --------------------------------------------------------------------- 39% The document has an index 40% --------------------------------------------------------------------- 41\makeindex 42 43\begin{document} 44 45 \setlength{\unitlength}{1mm} % unit of length = 1mm 46 \setlength{\baselineskip}{16pt} % line spacing = 16pt 47 48 % --------------------------------------------------------------------- 49 % prelims 50 % --------------------------------------------------------------------- 51 52 \pagenumbering{roman} % roman page numbers for prelims 53 \setcounter{page}{1} % start at page 1 54 55 \include{title} % title page 56 \tableofcontents % table of contents 57 58 % --------------------------------------------------------------------- 59 % Systematic description of the library 60 % --------------------------------------------------------------------- 61 62 \cleardoublepage % kick to a right-hand page 63 \pagenumbering{arabic} % arabic page numbers 64 \setcounter{page}{1} % start at page 1 65 \include{description} 66 67 % --------------------------------------------------------------------- 68 % Reference manual entries for functions 69 % --------------------------------------------------------------------- 70 71 \include{entries} 72 73 % --------------------------------------------------------------------- 74 % Listing of theorems 75 % --------------------------------------------------------------------- 76 77 \include{theorems} 78 79 % --------------------------------------------------------------------- 80 % References 81 % --------------------------------------------------------------------- 82 83 \include{references} 84 85 % --------------------------------------------------------------------- 86 % Index 87 % --------------------------------------------------------------------- 88 89 {\def\_{{\char'137}} % \tt style `_' character 90 91 \printindex } 92% \include{index}} 93 94\end{document} 95 96 97