# HG changeset patch
# User paulson
# Date 844861828 -7200
# Node ID 12eed4cec93576215f12b0710a58d8e51e8ad126
# Parent 8f0d199373a3700b7847a2f1bfe006c2518486ab
Fuller description of examples
diff -r 8f0d199373a3 -r 12eed4cec935 src/HOL/README.html
--- 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 @@
+
HOL/ReadMe
HOL: Higher-Order Logic with curried functions
@@ -12,10 +13,32 @@
Makefile
compiles the files under Poly/ML or SML of New Jersey
+
+
There are several subdirectories. To execute them, issue the command
+
+ use_dir "<DIR>";
+
+where <DIR> is the desired directory
+
+
- ex
-
- subdirectory containing examples. To execute them, enter an ML image
-containing HOL and type: use "ex/ROOT.ML";
+
- general examples
+
+
- Auth
+
- a new approach to verifying authentication protocols
+
+
- IMP
+
- mechanization of a large part of a semantics text by Glynn Winskel
+
+
- Integ
+
- a theory of the integers including efficient integer calculations
+
+
- IOA
+
- extended example of Input/Output Automata (takes a long time to run!)
+
+
- Lambda
+
- a proof of the Church-Rosser theorem for lambda-calculus
- Subst
- subdirectory defining a theory of substitution and unification.