summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

3 This directory contains the Standard ML sources of the Isabelle system for

4 Higher-Order Logic with curried functions. Important files include

6 ROOT.ML -- loads all source files. Enter an ML image containing Pure

7 Isabelle and type: use "ROOT.ML";

9 Makefile -- compiles the files under Poly/ML or SML of New Jersey

11 ex -- subdirectory containing examples. To execute them, enter an ML image

12 containing HOL and type: use "ex/ROOT.ML";

14 Subst -- subdirectory defining a theory of substitution and unification.

16 Useful references on Higher-Order Logic:

18 P. B. Andrews,

19 An Introduction to Mathematical Logic and Type Theory

20 (Academic Press, 1986).

22 J. Lambek and P. J. Scott,

23 Introduction to Higher Order Categorical Logic (CUP, 1986)