# HG changeset patch
# User paulson
# Date 933586264 -7200
# Node ID 3c664fbb291017d0359c9ddd917540ec406e83e8
# Parent  c05373eebee399dea55051cc8a371eb8d3bddd33
long-overdue updating

diff -r c05373eebee3 -r 3c664fbb2910 src/HOL/ex/README.html
--- 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>