--- a/src/HOL/ex/README.html Mon Jul 23 17:37:29 2001 +0200
+++ b/src/HOL/ex/README.html Mon Jul 23 17:45:07 2001 +0200
@@ -7,31 +7,29 @@
features of Isabelle/HOL.
<UL>
-<LI>Files <KBD>cla.ML</KBD> demonstrates the
+<LI>File <A HREF="cla.ML"><KBD>cla.ML</KBD></A> demonstrates the
power of Isabelle's classical reasoner.
-<LI>Files <KBD>meson.ML</KBD> and <KBD>mesontest.ML</KBD> present an
+<LI>Files <A HREF="mesontest.ML"><KBD>mesontest.ML</KBD></A> and
+<A HREF="mesontest2.ML"><KBD>mesontest2.ML</KBD></A> present an
implementation of the Model Elimination (ME) proof procedure, which is even
more powerful than the classical reasoner but not generic.
-<LI><KBD>InSort</KBD> and <KBD>Qsort</KBD> are correctness proofs for sorting
+<LI><A HREF="InSort.thy"><KBD>InSort</KBD></A> and <A HREF="Qsort.thy"><KBD>Qsort</KBD></A> are correctness proofs for sorting
functions.
-<LI><KBD>Primes</KBD> is a theory of the <EM>divides</EM> relation, the
-greatest common divisor and Euclid's algorithm.
+<LI><A HREF="Primrec.thy"><KBD>Primrec</KBD></A> proves that Ackermann's
+function is not primitive recursive.
-<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
+<LI><A HREF="Tarski.thy"><KBD>Tarski</KBD></A> 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.
+<LI><A HREF="NatSum.thy"><KBD>NatSum</KBD></A> demonstrates the power of permutative rewriting.
Well-known identities about summations are proved using just induction and
rewriting.
-<LI><KBD>MT</KBD> is a preliminary version of Jacob Frost's coinduction
+<LI><A HREF="MT.thy"><KBD>MT</KBD></A> is a preliminary version of Jacob Frost's coinduction
example. The full version is on the directory <KBD>ZF/Coind</KBD>.
</UL>