src/HOL/Induct/README.html
changeset 5417 1f533238b53b
parent 3122 2fe26ca380a1
child 11053 026007eb2ccc
--- 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>).