src/HOL/README.html
author paulson
Wed May 07 13:51:22 1997 +0200 (1997-05-07)
changeset 3125 3f0ab2c306f7
parent 2080 12eed4cec935
child 3279 815ef5848324
permissions -rw-r--r--
Moved induction examples to directory Induct
     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>Induct
    35 <DD>examples of (co)inductive definitions
    36 
    37 <DT>Integ
    38 <DD>a theory of the integers including efficient integer calculations
    39 
    40 <DT>IOA
    41 <DD>extended example of Input/Output Automata
    42 
    43 <DT>Lambda
    44 <DD>a proof of the Church-Rosser theorem for lambda-calculus
    45 
    46 <DT>Subst
    47 <DD>subdirectory defining a theory of substitution and unification.
    48 </DL>
    49 
    50 Useful references on Higher-Order Logic:
    51 
    52 <UL>
    53 <LI>P. B. Andrews,<BR>
    54     An Introduction to Mathematical Logic and Type Theory<BR>
    55     (Academic Press, 1986).
    56 
    57 <LI>J. Lambek and P. J. Scott,<BR>
    58     Introduction to Higher Order Categorical Logic (CUP, 1986)
    59 </UL>
    60 
    61 </BODY></HTML>