src/HOL/README
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1339 f1a3a7b44ff1
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
     1 	   HOL: Higher-Order Logic with curried functions
     2 
     3 This directory contains the Standard ML sources of the Isabelle system for
     4 Higher-Order Logic with curried functions.  Important files include
     5 
     6 ROOT.ML -- loads all source files.  Enter an ML image containing Pure
     7 Isabelle and type:    use "ROOT.ML";
     8 
     9 Makefile -- compiles the files under Poly/ML or SML of New Jersey
    10 
    11 ex -- subdirectory containing examples.  To execute them, enter an ML image
    12 containing HOL and type:    use "ex/ROOT.ML";
    13 
    14 Subst -- subdirectory defining a theory of substitution and unification.
    15 
    16 Useful references on Higher-Order Logic:
    17 
    18 	P. B. Andrews,
    19 	An Introduction to Mathematical Logic and Type Theory
    20 	(Academic Press, 1986).
    21 
    22 	J. Lambek and P. J. Scott,
    23 	Introduction to Higher Order Categorical Logic (CUP, 1986)