src/HOL/README.html
author paulson
Wed Oct 09 13:50:28 1996 +0200 (1996-10-09)
changeset 2080 12eed4cec935
parent 1341 69fec018854c
child 3125 3f0ab2c306f7
permissions -rw-r--r--
Fuller description of examples
paulson@2080
     1
<!-- $Id$ -->
clasohm@1339
     2
<HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
clasohm@1339
     3
clasohm@1339
     4
<H2>HOL: Higher-Order Logic with curried functions</H2>
clasohm@1339
     5
clasohm@1339
     6
This directory contains the Standard ML sources of the Isabelle system for
clasohm@1339
     7
Higher-Order Logic with curried functions.  Important files include
clasohm@1339
     8
clasohm@1339
     9
<DL>
clasohm@1339
    10
<DT>ROOT.ML
clasohm@1339
    11
<DD>loads all source files.  Enter an ML image containing Pure
clasohm@1339
    12
Isabelle and type: use "ROOT.ML";<P>
clasohm@1339
    13
clasohm@1339
    14
<DT>Makefile
clasohm@1339
    15
<DD>compiles the files under Poly/ML or SML of New Jersey<P>
paulson@2080
    16
</DL>
clasohm@1339
    17
paulson@2080
    18
<P>There are several subdirectories.  To execute them, issue the command
paulson@2080
    19
<PRE>
paulson@2080
    20
        use_dir "<I>&lt;DIR&gt;</I>";
paulson@2080
    21
</PRE>
paulson@2080
    22
where <I>&lt;DIR&gt;</I> is the desired directory 
paulson@2080
    23
paulson@2080
    24
<DL>
clasohm@1339
    25
<DT>ex
paulson@2080
    26
<DD>general examples
paulson@2080
    27
paulson@2080
    28
<DT>Auth
paulson@2080
    29
<DD>a new approach to verifying authentication protocols 
paulson@2080
    30
paulson@2080
    31
<DT>IMP
paulson@2080
    32
<DD>mechanization of a large part of a semantics text by Glynn Winskel
paulson@2080
    33
paulson@2080
    34
<DT>Integ
paulson@2080
    35
<DD>a theory of the integers including efficient integer calculations
paulson@2080
    36
paulson@2080
    37
<DT>IOA
paulson@2080
    38
<DD>extended example of Input/Output Automata (takes a long time to run!)
paulson@2080
    39
paulson@2080
    40
<DT>Lambda
paulson@2080
    41
<DD>a proof of the Church-Rosser theorem for lambda-calculus
clasohm@1339
    42
clasohm@1339
    43
<DT>Subst
clasohm@1339
    44
<DD>subdirectory defining a theory of substitution and unification.
clasohm@1339
    45
</DL>
clasohm@1339
    46
clasohm@1339
    47
Useful references on Higher-Order Logic:
clasohm@1339
    48
clasohm@1339
    49
<UL>
clasohm@1341
    50
<LI>P. B. Andrews,<BR>
clasohm@1341
    51
    An Introduction to Mathematical Logic and Type Theory<BR>
clasohm@1341
    52
    (Academic Press, 1986).
clasohm@1339
    53
clasohm@1341
    54
<LI>J. Lambek and P. J. Scott,<BR>
clasohm@1341
    55
    Introduction to Higher Order Categorical Logic (CUP, 1986)
clasohm@1339
    56
</UL>
clasohm@1339
    57
clasohm@1339
    58
</BODY></HTML>