equal
deleted
inserted
replaced
6 \urlstyle{rm} |
6 \urlstyle{rm} |
7 \isabellestyle{it} |
7 \isabellestyle{it} |
8 |
8 |
9 \begin{document} |
9 \begin{document} |
10 |
10 |
11 \title{Examples of Inductive and Coinductive Definitions} |
11 \title{Examples of Inductive and Coinductive Definitions in HOL} |
12 \author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel} |
12 \author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel} |
13 \maketitle |
13 \maketitle |
14 |
14 |
15 \begin{abstract} |
15 \begin{abstract} |
16 This is a collection of small examples to demonstrate Isabelle/HOL's |
16 This is a collection of small examples to demonstrate Isabelle/HOL's |