--- 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: