src/HOL/Induct/document/root.tex
author haftmann
Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417 9bc16273c2d4
parent 12185 54bd9aa3343d
child 61993 89206877f0ee
permissions -rw-r--r--
migrated theory headers to new format
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     1
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     2
\documentclass[11pt,a4paper]{article}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     3
\usepackage{isabelle,isabellesym,pdfsetup}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     4
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     5
%for best-style documents ...
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     6
\urlstyle{rm}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     7
\isabellestyle{it}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     8
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     9
\begin{document}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    10
12185
wenzelm
parents: 11046
diff changeset
    11
\title{Examples of Inductive and Coinductive Definitions in HOL}
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    12
\author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    13
\maketitle
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    14
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    15
\begin{abstract}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    16
  This is a collection of small examples to demonstrate Isabelle/HOL's
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    17
  (co)inductive definitions package.  Large examples appear on many other
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    18
  sessions, such as Lambda, IMP, and Auth.
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    19
\end{abstract}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    20
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    21
\tableofcontents
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    22
\newpage
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    23
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    24
\parindent 0pt\parskip 0.5ex
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    25
\input{session}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    26
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    27
\end{document}