equal
deleted
inserted
replaced
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) |
|