src/HOLCF/README.html
changeset 6034 96ac04a17c56
parent 3279 815ef5848324
child 15255 1b860b5d23f8
     1.1 --- a/src/HOLCF/README.html	Fri Dec 18 11:01:25 1998 +0100
     1.2 +++ b/src/HOLCF/README.html	Fri Dec 18 19:43:10 1998 +0100
     1.3 @@ -2,8 +2,17 @@
     1.4  
     1.5  <H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
     1.6  
     1.7 -Author:     Franz Regensburger<BR>
     1.8 -Copyright   1995 Technische Universität München<P>
     1.9 +HOLCF is the definitional extension of Church's Higher-Order Logic with
    1.10 +Scott's Logic for Computable Functions that has been implemented in the
    1.11 +theorem prover Isabelle.  This results in a flexible setup for reasoning
    1.12 +about functional programs. HOLCF supports standard domain theory (in particular
    1.13 +fixpoint reasoning and recursive domain equations) but also coinductive
    1.14 +arguments about lazy datatypes.
    1.15 +<P>
    1.16 +The most recent description of HOLCF is found here:
    1.17 +<UL>
    1.18 +<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
    1.19 +</UL>
    1.20  
    1.21  A detailed description (in german) of the entire development can be found in:
    1.22