--- a/src/HOL/ex/README.html Mon Aug 02 11:29:13 1999 +0200
+++ b/src/HOL/ex/README.html Mon Aug 02 11:31:04 1999 +0200
@@ -20,6 +20,13 @@
<LI><KBD>Primes</KBD> is a theory of the <EM>divides</EM> relation, the
greatest common divisor and Euclid's algorithm.
+<LI><KBD>Fib</KBD> proves some theorems (some rather difficult) about the
+Fibonacci function.
+
+<LI><KBD>Tarski</KBD> is a proof of Tarski's fixedpoint theorem: the full
+version, which states that the fixedpoints of a complete lattice themselves
+form a complete lattice. The example demonstrates first-class reasoning about theories.
+
<LI><KBD>NatSum</KBD> demonstrates the power of permutative rewriting.
Well-known identities about summations are proved using just induction and
rewriting.
@@ -29,7 +36,7 @@
</UL>
<HR>
-<P>Last modified 6 May 1997
+<P>Last modified on $Date$
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>