src/HOL/README.html
author clasohm
Fri Nov 17 12:40:09 1995 +0100 (1995-11-17)
changeset 1339 f1a3a7b44ff1
child 1341 69fec018854c
permissions -rw-r--r--
converted README to HTLM; replaced "CHOL" by "HOL"
     1 <HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
     2 
     3 <H2>HOL: Higher-Order Logic with curried functions</H2>
     4 
     5 This directory contains the Standard ML sources of the Isabelle system for
     6 Higher-Order Logic with curried functions.  Important files include
     7 
     8 <DL>
     9 <DT>ROOT.ML
    10 <DD>loads all source files.  Enter an ML image containing Pure
    11 Isabelle and type: use "ROOT.ML";<P>
    12 
    13 <DT>Makefile
    14 <DD>compiles the files under Poly/ML or SML of New Jersey<P>
    15 
    16 <DT>ex
    17 <DD>subdirectory containing examples.  To execute them, enter an ML image
    18 containing HOL and type: use "ex/ROOT.ML";<P>
    19 
    20 <DT>Subst
    21 <DD>subdirectory defining a theory of substitution and unification.
    22 </DL>
    23 
    24 Useful references on Higher-Order Logic:
    25 
    26 <UL>
    27 <LI>P. B. Andrews, An Introduction to Mathematical Logic and Type Theory
    28 (Academic Press, 1986).
    29 
    30 <LI>J. Lambek and P. J. Scott, Introduction to Higher Order
    31 Categorical Logic (CUP, 1986)
    32 </UL>
    33 
    34 </BODY></HTML>