doc-src/Inductive/ind-defs.tex

 %% $Id$
 \documentclass[12pt]{article}
-\usepackage{a4,latexsym,../iman,../extra,../proof}
+\usepackage{a4,latexsym,../iman,../extra,../proof,../pdfsetup}
 
 \newif\ifshort%''Short'' means a published version, not the documentation
 \shortfalse%%%%%\shorttrue
 
 \title{A Fixedpoint Approach to\\ 

 \[ \infer{\pair{m\mathbin{+} m',\, l@l'}\in\listn(A)}
          {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} 
 \]
 where $+$ denotes addition on the natural numbers and @ denotes append.
 
-\subsection{Rule inversion: the function {\tt mk\_cases}}
+\subsection{Rule inversion: the function \texttt{mk\_cases}}
 The elimination rule, {\tt listn.elim}, is cumbersome:
 \[ \infer{Q}{x\in\listn(A) & 
           \infer*{Q}{[x = \pair{0,\Nil}]} &
           \infer*{Q}
              {\left[\begin{array}{l}

 ported the (co)inductive definition package from Isabelle/\textsc{zf} to
 Isabelle/\textsc{hol} (higher-order logic).  
 
 
 \begin{footnotesize}
-\bibliographystyle{springer}
+\bibliographystyle{plain}
 \bibliography{../manual}
 \end{footnotesize}
 %%%%%\doendnotes
 
 \end{document}