Fuller description of examples
authorpaulson
Wed Oct 09 13:50:28 1996 +0200 (1996-10-09)
changeset 208012eed4cec935
parent 2079 8f0d199373a3
child 2081 c2da3ca231ab
Fuller description of examples
src/HOL/README.html
     1.1 --- a/src/HOL/README.html	Wed Oct 09 13:47:38 1996 +0200
     1.2 +++ b/src/HOL/README.html	Wed Oct 09 13:50:28 1996 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +<!-- $Id$ -->
     1.5  <HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
     1.6  
     1.7  <H2>HOL: Higher-Order Logic with curried functions</H2>
     1.8 @@ -12,10 +13,32 @@
     1.9  
    1.10  <DT>Makefile
    1.11  <DD>compiles the files under Poly/ML or SML of New Jersey<P>
    1.12 +</DL>
    1.13  
    1.14 +<P>There are several subdirectories.  To execute them, issue the command
    1.15 +<PRE>
    1.16 +        use_dir "<I>&lt;DIR&gt;</I>";
    1.17 +</PRE>
    1.18 +where <I>&lt;DIR&gt;</I> is the desired directory 
    1.19 +
    1.20 +<DL>
    1.21  <DT>ex
    1.22 -<DD>subdirectory containing examples.  To execute them, enter an ML image
    1.23 -containing HOL and type: use "ex/ROOT.ML";<P>
    1.24 +<DD>general examples
    1.25 +
    1.26 +<DT>Auth
    1.27 +<DD>a new approach to verifying authentication protocols 
    1.28 +
    1.29 +<DT>IMP
    1.30 +<DD>mechanization of a large part of a semantics text by Glynn Winskel
    1.31 +
    1.32 +<DT>Integ
    1.33 +<DD>a theory of the integers including efficient integer calculations
    1.34 +
    1.35 +<DT>IOA
    1.36 +<DD>extended example of Input/Output Automata (takes a long time to run!)
    1.37 +
    1.38 +<DT>Lambda
    1.39 +<DD>a proof of the Church-Rosser theorem for lambda-calculus
    1.40  
    1.41  <DT>Subst
    1.42  <DD>subdirectory defining a theory of substitution and unification.