# HG changeset patch
# User nipkow
# Date 914006590 -3600
# Node ID 96ac04a17c5621c2fdd065a66e4c2fe85e22ee30
# Parent  c8c69a4a7762124b8550a580b1be6b5d4232d8fb
Link to HOLCF paper added.

diff -r c8c69a4a7762 -r 96ac04a17c56 src/HOLCF/README.html
--- 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: