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