--- a/src/HOLCF/README.html Fri Dec 18 11:01:25 1998 +0100
+++ b/src/HOLCF/README.html Fri Dec 18 19:43:10 1998 +0100
@@ -2,8 +2,17 @@
<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
-Author: Franz Regensburger<BR>
-Copyright 1995 Technische Universität München<P>
+HOLCF is the definitional extension of Church's Higher-Order Logic with
+Scott's Logic for Computable Functions that has been implemented in the
+theorem prover Isabelle. This results in a flexible setup for reasoning
+about functional programs. HOLCF supports standard domain theory (in particular
+fixpoint reasoning and recursive domain equations) but also coinductive
+arguments about lazy datatypes.
+<P>
+The most recent description of HOLCF is found here:
+<UL>
+<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
+</UL>
A detailed description (in german) of the entire development can be found in: