## Induct--Examples of (Co)Inductive Definitions

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

`Comb` proves the Church-Rosser theorem for combinators (paper
available).
`Mutil` is the famous Mutilated Chess Board problem (paper
available).
`PropLog` proves the completeness of a formalization of
propositional logic (paper
available).
`LFilter` is an inductive/corecursive formalization of the
*filter* functional for infinite streams.
`Exp` demonstrates the use of iterated inductive definitions to
reason about mutually recursive relations.

lcp@cl.cam.ac.uk