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
clasohm@1339
     1
	   HOL: Higher-Order Logic with curried functions
clasohm@923
     2
clasohm@923
     3
This directory contains the Standard ML sources of the Isabelle system for
clasohm@923
     4
Higher-Order Logic with curried functions.  Important files include
clasohm@923
     5
clasohm@923
     6
ROOT.ML -- loads all source files.  Enter an ML image containing Pure
clasohm@923
     7
Isabelle and type:    use "ROOT.ML";
clasohm@923
     8
clasohm@923
     9
Makefile -- compiles the files under Poly/ML or SML of New Jersey
clasohm@923
    10
clasohm@923
    11
ex -- subdirectory containing examples.  To execute them, enter an ML image
clasohm@1339
    12
containing HOL and type:    use "ex/ROOT.ML";
clasohm@923
    13
clasohm@923
    14
Subst -- subdirectory defining a theory of substitution and unification.
clasohm@923
    15
clasohm@923
    16
Useful references on Higher-Order Logic:
clasohm@923
    17
clasohm@923
    18
	P. B. Andrews,
clasohm@923
    19
	An Introduction to Mathematical Logic and Type Theory
clasohm@923
    20
	(Academic Press, 1986).
clasohm@923
    21
clasohm@923
    22
	J. Lambek and P. J. Scott,
clasohm@923
    23
	Introduction to Higher Order Categorical Logic (CUP, 1986)