1.1 --- a/doc-src/Inductive/ind-defs.tex Wed May 12 09:44:44 1999 +0200
1.2 +++ b/doc-src/Inductive/ind-defs.tex Wed May 12 11:01:01 1999 +0200
1.3 @@ -1,6 +1,6 @@
1.4 %% $Id$
1.5 \documentclass[12pt]{article}
1.6 -\usepackage{a4,latexsym,../iman,../extra,../proof}
1.7 +\usepackage{a4,latexsym,../iman,../extra,../proof,../pdfsetup}
1.8
1.9 \newif\ifshort%''Short'' means a published version, not the documentation
1.10 \shortfalse%%%%%\shorttrue
1.11 @@ -614,7 +614,7 @@
1.12 \]
1.13 where $+$ denotes addition on the natural numbers and @ denotes append.
1.14
1.15 -\subsection{Rule inversion: the function {\tt mk\_cases}}
1.16 +\subsection{Rule inversion: the function \texttt{mk\_cases}}
1.17 The elimination rule, {\tt listn.elim}, is cumbersome:
1.18 \[ \infer{Q}{x\in\listn(A) &
1.19 \infer*{Q}{[x = \pair{0,\Nil}]} &
1.20 @@ -1326,7 +1326,7 @@
1.21
1.22
1.23 \begin{footnotesize}
1.24 -\bibliographystyle{springer}
1.25 +\bibliographystyle{plain}
1.26 \bibliography{../manual}
1.27 \end{footnotesize}
1.28 %%%%%\doendnotes