\title{Examples of Inductive and Coinductive Definitions in HOL} \author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel} \maketitle
\begin{abstract}
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. \end{abstract}
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
