src/HOL/README.html
author wenzelm
Tue, 20 May 1997 19:29:50 +0200
changeset 3257 4e3724e0659f
parent 3125 3f0ab2c306f7
child 3279 815ef5848324
permissions -rw-r--r--
README generation;

<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>

<H2>HOL: Higher-Order Logic with curried functions</H2>

This directory contains the Standard ML sources of the Isabelle system for
Higher-Order Logic with curried functions.  Important files include

<DL>
<DT>ROOT.ML
<DD>loads all source files.  Enter an ML image containing Pure
Isabelle and type: use "ROOT.ML";<P>

<DT>Makefile
<DD>compiles the files under Poly/ML or SML of New Jersey<P>
</DL>

<P>There are several subdirectories.  To execute them, issue the command
<PRE>
        use_dir "<I>&lt;DIR&gt;</I>";
</PRE>
where <I>&lt;DIR&gt;</I> is the desired directory 

<DL>
<DT>ex
<DD>general examples

<DT>Auth
<DD>a new approach to verifying authentication protocols 

<DT>IMP
<DD>mechanization of a large part of a semantics text by Glynn Winskel

<DT>Induct
<DD>examples of (co)inductive definitions

<DT>Integ
<DD>a theory of the integers including efficient integer calculations

<DT>IOA
<DD>extended example of Input/Output Automata

<DT>Lambda
<DD>a proof of the Church-Rosser theorem for lambda-calculus

<DT>Subst
<DD>subdirectory defining a theory of substitution and unification.
</DL>

Useful references on Higher-Order Logic:

<UL>
<LI>P. B. Andrews,<BR>
    An Introduction to Mathematical Logic and Type Theory<BR>
    (Academic Press, 1986).

<LI>J. Lambek and P. J. Scott,<BR>
    Introduction to Higher Order Categorical Logic (CUP, 1986)
</UL>

</BODY></HTML>