changeset 6034 96ac04a17c56
parent 3279 815ef5848324
child 15255 1b860b5d23f8
--- 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.
+The most recent description of HOLCF is found here:
+<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
 A detailed description (in german) of the entire development can be found in: