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


%for best-style documents ...


\title{Examples of Inductive and Coinductive Definitions in HOL}
\author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel}

  This is a collection of small examples to demonstrate Isabelle/HOL's
  (co)inductive definitions package.  Large examples appear on many other
  sessions, such as Lambda, IMP, and Auth.


\parindent 0pt\parskip 0.5ex