doc-src/Inductive/ind-defs.tex
changeset 6637 57abed64dc14
parent 6631 ccae8c659762
child 6745 74e8f703f5f2
     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