summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/README

author | clasohm |

Fri, 17 Nov 1995 12:40:09 +0100 | |

changeset 1339 | f1a3a7b44ff1 |

parent 923 | ff1574a81019 |

permissions | -rw-r--r-- |

converted README to HTLM; replaced "CHOL" by "HOL"

HOL: Higher-Order Logic with curried functions This directory contains the Standard ML sources of the Isabelle system for Higher-Order Logic with curried functions. Important files include ROOT.ML -- loads all source files. Enter an ML image containing Pure Isabelle and type: use "ROOT.ML"; Makefile -- compiles the files under Poly/ML or SML of New Jersey ex -- subdirectory containing examples. To execute them, enter an ML image containing HOL and type: use "ex/ROOT.ML"; Subst -- subdirectory defining a theory of substitution and unification. Useful references on Higher-Order Logic: P. B. Andrews, An Introduction to Mathematical Logic and Type Theory (Academic Press, 1986). J. Lambek and P. J. Scott, Introduction to Higher Order Categorical Logic (CUP, 1986)