paulson@2080: clasohm@1339: HOL/ReadMe clasohm@1339: clasohm@1339:

HOL: Higher-Order Logic with curried functions

clasohm@1339: clasohm@1339: This directory contains the Standard ML sources of the Isabelle system for clasohm@1339: Higher-Order Logic with curried functions. Important files include clasohm@1339: clasohm@1339:
clasohm@1339:
ROOT.ML clasohm@1339:
loads all source files. Enter an ML image containing Pure clasohm@1339: Isabelle and type: use "ROOT.ML";

clasohm@1339: clasohm@1339:

Makefile clasohm@1339:
compiles the files under Poly/ML or SML of New Jersey

paulson@2080:

clasohm@1339: paulson@2080:

There are several subdirectories. To execute them, issue the command paulson@2080: 

paulson@2080:         use_dir "<DIR>";
paulson@2080:
paulson@2080: where <DIR> is the desired directory paulson@2080: paulson@2080:
clasohm@1339:
ex paulson@2080:
general examples paulson@2080: paulson@2080:
Auth paulson@2080:
a new approach to verifying authentication protocols paulson@2080: paulson@2080:
IMP paulson@2080:
mechanization of a large part of a semantics text by Glynn Winskel paulson@2080: paulson@2080:
Integ paulson@2080:
a theory of the integers including efficient integer calculations paulson@2080: paulson@2080:
IOA paulson@2080:
extended example of Input/Output Automata (takes a long time to run!) paulson@2080: paulson@2080:
Lambda paulson@2080:
a proof of the Church-Rosser theorem for lambda-calculus clasohm@1339: clasohm@1339:
Subst clasohm@1339:
subdirectory defining a theory of substitution and unification. clasohm@1339:
clasohm@1339: clasohm@1339: Useful references on Higher-Order Logic: clasohm@1339: clasohm@1339: clasohm@1339: clasohm@1339: