# HG changeset patch
# User paulson
# Date 863005797 -7200
# Node ID 2fe26ca380a1ce87f99eba64b6253b7537426ad5
# Parent cbb6c0c1c58ae91ff5046b9cc6df9ed4c3fc7666
Documentation for directory "Induct"
diff -r cbb6c0c1c58a -r 2fe26ca380a1 src/HOL/Induct/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/README.html Wed May 07 13:49:57 1997 +0200
@@ -0,0 +1,39 @@
+
+HOL/Induct/README
+
+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.
+
+
+- Perm is a simple theory of permutations of lists.
+
+
- 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.
+
+
+
+Last modified 7 May 1997
+
+
+lcp@cl.cam.ac.uk
+
+