src/HOL/README.html
author clasohm
Fri Nov 17 13:22:50 1995 +0100 (1995-11-17)
changeset 1341 69fec018854c
parent 1339 f1a3a7b44ff1
child 2080 12eed4cec935
permissions -rw-r--r--
HTML version of README
     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,<BR>
    28     An Introduction to Mathematical Logic and Type Theory<BR>
    29     (Academic Press, 1986).
    30 
    31 <LI>J. Lambek and P. J. Scott,<BR>
    32     Introduction to Higher Order Categorical Logic (CUP, 1986)
    33 </UL>
    34 
    35 </BODY></HTML>