--- a/src/HOL/Induct/README.html Tue Sep 01 15:04:28 1998 +0200
+++ b/src/HOL/Induct/README.html Tue Sep 01 15:04:59 1998 +0200
@@ -10,6 +10,13 @@
<UL>
<LI><KBD>Perm</KBD> is a simple theory of permutations of lists.
+<LI><KBD>FoldSet</KBD> declares a <EM>fold</EM> functional for finite sets.
+Let f be an associative-commutative function with identity e.
+For n non-negative we have
+<PRE>
+fold f e {x1,...,xn} = f x1 (... (f xn e))
+</PRE>
+
<LI><KBD>Comb</KBD> proves the Church-Rosser theorem for combinators (<A
HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz">paper
available</A>).