src/HOL/README.html
author wenzelm
Wed May 21 17:13:00 1997 +0200 (1997-05-21)
changeset 3279 815ef5848324
parent 3125 3f0ab2c306f7
child 4622 85aae356570c
permissions -rw-r--r--
tuned all READMEs;
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
     3 
     4 <H2>HOL: Higher-Order Logic</H2>
     5 
     6 This directory contains the ML sources of the Isabelle system for
     7 Higher-Order Logic.<P>
     8 
     9 There are several subdirectories with examples:
    10 <DL>
    11 <DT>ex
    12 <DD>general examples
    13 
    14 <DT>Auth
    15 <DD>a new approach to verifying authentication protocols 
    16 
    17 <DT>IMP
    18 <DD>mechanization of a large part of a semantics text by Glynn Winskel
    19 
    20 <DT>Induct
    21 <DD>examples of (co)inductive definitions
    22 
    23 <DT>Integ
    24 <DD>a theory of the integers including efficient integer calculations
    25 
    26 <DT>IOA
    27 <DD>extended example of Input/Output Automata
    28 
    29 <DT>Lambda
    30 <DD>a proof of the Church-Rosser theorem for lambda-calculus
    31 
    32 <DT>Subst
    33 <DD>subdirectory defining a theory of substitution and unification.
    34 </DL>
    35 
    36 Useful references on Higher-Order Logic:
    37 
    38 <UL>
    39 <LI>P. B. Andrews,<BR>
    40     An Introduction to Mathematical Logic and Type Theory<BR>
    41     (Academic Press, 1986).
    42 
    43 <LI>J. Lambek and P. J. Scott,<BR>
    44     Introduction to Higher Order Categorical Logic (CUP, 1986)
    45 </UL>
    46 
    47 </BODY></HTML>