Fuller description of examples
Wed, 09 Oct 1996 13:50:28 +0200
changeset 2080 12eed4cec935
parent 2079 8f0d199373a3
child 2081 c2da3ca231ab
Fuller description of examples
--- a/src/HOL/README.html	Wed Oct 09 13:47:38 1996 +0200
+++ b/src/HOL/README.html	Wed Oct 09 13:50:28 1996 +0200
@@ -1,3 +1,4 @@
+<!-- $Id$ -->
 <H2>HOL: Higher-Order Logic with curried functions</H2>
@@ -12,10 +13,32 @@
 <DD>compiles the files under Poly/ML or SML of New Jersey<P>
+<P>There are several subdirectories.  To execute them, issue the command
+        use_dir "<I>&lt;DIR&gt;</I>";
+where <I>&lt;DIR&gt;</I> is the desired directory 
-<DD>subdirectory containing examples.  To execute them, enter an ML image
-containing HOL and type: use "ex/ROOT.ML";<P>
+<DD>general examples
+<DD>a new approach to verifying authentication protocols 
+<DD>mechanization of a large part of a semantics text by Glynn Winskel
+<DD>a theory of the integers including efficient integer calculations
+<DD>extended example of Input/Output Automata (takes a long time to run!)
+<DD>a proof of the Church-Rosser theorem for lambda-calculus
 <DD>subdirectory defining a theory of substitution and unification.