# HG changeset patch
# User nipkow
# Date 935075165 -7200
# Node ID 8aa66ddc0bea0f110e8771abba1b30e0c80d46a9
# Parent  f1a37c379317c3348c3730057c29aa488b91e74d
new entriues.

diff -r f1a37c379317 -r 8aa66ddc0bea src/HOL/README.html
--- a/src/HOL/README.html	Thu Aug 19 16:54:38 1999 +0200
+++ b/src/HOL/README.html	Thu Aug 19 17:06:05 1999 +0200
@@ -14,6 +14,10 @@
 <DT>Auth
 <DD>a new approach to verifying authentication protocols 
 
+<DT>Hoare
+<DD>verification of imperative programs; verification conditions are
+generated automatically from pre/post conditions and loop invariants.
+
 <DT>IMP
 <DD>mechanization of a large part of a semantics text by Glynn Winskel
 
@@ -25,11 +29,17 @@
 calculations (part of the standard HOL environment)
 
 <DT>IOA
-<DD>extended example of Input/Output Automata
+<DD>a simple theory of Input/Output Automata
 
 <DT>Lambda
 <DD>a proof of the Church-Rosser theorem for lambda-calculus
 
+<DT>Lex
+<DD>verification of a simple lexical analyzer generator
+
+<DT>MiniML
+<DD>formalization of type inference for the language Mini-ML
+
 <DT>Real 
 <DD>a development of the reals and hyper-reals, which are used in
 non-standard analysis.  Also includes the positive rationals.  Used to build
@@ -38,11 +48,17 @@
 <DT>Subst
 <DD>defines a theory of substitution and unification.
 
+<DT>TLA
+<DD>Lamport's Temporal Logic of Actions
+
 <DT>Tools
 <DD>holds code used to provide support for records, datatypes, induction, etc.
 
 <DT>UNITY
 <DD>Chandy and Misra's UNITY formalism.
+
+<DT>W0
+<DD>a precursor of MiniML, without let-expressions
 </DL>
 
 Useful references on Higher-Order Logic: