src/HOL/Induct/document/root.tex
changeset 11046 b5f5942781a0
child 12185 54bd9aa3343d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Induct/document/root.tex	Sat Feb 03 17:40:16 2001 +0100
     1.3 @@ -0,0 +1,27 @@
     1.4 +
     1.5 +\documentclass[11pt,a4paper]{article}
     1.6 +\usepackage{isabelle,isabellesym,pdfsetup}
     1.7 +
     1.8 +%for best-style documents ...
     1.9 +\urlstyle{rm}
    1.10 +\isabellestyle{it}
    1.11 +
    1.12 +\begin{document}
    1.13 +
    1.14 +\title{Examples of Inductive and Coinductive Definitions}
    1.15 +\author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel}
    1.16 +\maketitle
    1.17 +
    1.18 +\begin{abstract}
    1.19 +  This is a collection of small examples to demonstrate Isabelle/HOL's
    1.20 +  (co)inductive definitions package.  Large examples appear on many other
    1.21 +  sessions, such as Lambda, IMP, and Auth.
    1.22 +\end{abstract}
    1.23 +
    1.24 +\tableofcontents
    1.25 +\newpage
    1.26 +
    1.27 +\parindent 0pt\parskip 0.5ex
    1.28 +\input{session}
    1.29 +
    1.30 +\end{document}