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.


lcp@cl.cam.ac.uk