| 12193 |      1 | \documentclass[11pt,a4paper]{article}
 | 
|  |      2 | \usepackage{isabelle,isabellesym}
 | 
| 40945 |      3 | \usepackage[utf8]{inputenc}
 | 
| 12193 |      4 | \usepackage{pdfsetup}
 | 
|  |      5 | 
 | 
|  |      6 | \urlstyle{rm}
 | 
|  |      7 | \isabellestyle{it}
 | 
|  |      8 | 
 | 
|  |      9 | 
 | 
|  |     10 | \begin{document}
 | 
|  |     11 | 
 | 
|  |     12 | \title{Examples of Inductive and Coinductive Definitions in ZF}
 | 
|  |     13 | \author{Lawrence C Paulson and others}
 | 
|  |     14 | \maketitle
 | 
|  |     15 | 
 | 
|  |     16 | \tableofcontents
 | 
|  |     17 | 
 | 
|  |     18 | \parindent 0pt\parskip 0.5ex
 | 
|  |     19 | \input{session}
 | 
|  |     20 | 
 | 
| 12610 |     21 | \bibliographystyle{abbrv}
 | 
|  |     22 | \bibliography{root}
 | 
|  |     23 | 
 | 
| 12193 |     24 | \end{document}
 |