converted README to HTLM; replaced "CHOL" by "HOL"
authorclasohm
Fri Nov 17 12:40:09 1995 +0100 (1995-11-17)
changeset 1339f1a3a7b44ff1
parent 1338 d2fc3bfaee7f
child 1340 71b0a5d83347
converted README to HTLM; replaced "CHOL" by "HOL"
src/HOL/README
src/HOL/README.html
     1.1 --- a/src/HOL/README	Fri Nov 17 12:19:21 1995 +0100
     1.2 +++ b/src/HOL/README	Fri Nov 17 12:40:09 1995 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -	   CHOL: Higher-Order Logic with curried functions
     1.5 +	   HOL: Higher-Order Logic with curried functions
     1.6  
     1.7  This directory contains the Standard ML sources of the Isabelle system for
     1.8  Higher-Order Logic with curried functions.  Important files include
     1.9 @@ -9,7 +9,7 @@
    1.10  Makefile -- compiles the files under Poly/ML or SML of New Jersey
    1.11  
    1.12  ex -- subdirectory containing examples.  To execute them, enter an ML image
    1.13 -containing CHOL and type:    use "ex/ROOT.ML";
    1.14 +containing HOL and type:    use "ex/ROOT.ML";
    1.15  
    1.16  Subst -- subdirectory defining a theory of substitution and unification.
    1.17  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/README.html	Fri Nov 17 12:40:09 1995 +0100
     2.3 @@ -0,0 +1,34 @@
     2.4 +<HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
     2.5 +
     2.6 +<H2>HOL: Higher-Order Logic with curried functions</H2>
     2.7 +
     2.8 +This directory contains the Standard ML sources of the Isabelle system for
     2.9 +Higher-Order Logic with curried functions.  Important files include
    2.10 +
    2.11 +<DL>
    2.12 +<DT>ROOT.ML
    2.13 +<DD>loads all source files.  Enter an ML image containing Pure
    2.14 +Isabelle and type: use "ROOT.ML";<P>
    2.15 +
    2.16 +<DT>Makefile
    2.17 +<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    2.18 +
    2.19 +<DT>ex
    2.20 +<DD>subdirectory containing examples.  To execute them, enter an ML image
    2.21 +containing HOL and type: use "ex/ROOT.ML";<P>
    2.22 +
    2.23 +<DT>Subst
    2.24 +<DD>subdirectory defining a theory of substitution and unification.
    2.25 +</DL>
    2.26 +
    2.27 +Useful references on Higher-Order Logic:
    2.28 +
    2.29 +<UL>
    2.30 +<LI>P. B. Andrews, An Introduction to Mathematical Logic and Type Theory
    2.31 +(Academic Press, 1986).
    2.32 +
    2.33 +<LI>J. Lambek and P. J. Scott, Introduction to Higher Order
    2.34 +Categorical Logic (CUP, 1986)
    2.35 +</UL>
    2.36 +
    2.37 +</BODY></HTML>