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 @@
Auth
a new approach to verifying authentication protocols
+Hoare
+verification of imperative programs; verification conditions are
+generated automatically from pre/post conditions and loop invariants.
+
IMP
mechanization of a large part of a semantics text by Glynn Winskel
@@ -25,11 +29,17 @@
calculations (part of the standard HOL environment)
IOA
-extended example of Input/Output Automata
+a simple theory of Input/Output Automata
Lambda
a proof of the Church-Rosser theorem for lambda-calculus
+Lex
+verification of a simple lexical analyzer generator
+
+MiniML
+formalization of type inference for the language Mini-ML
+
Real
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 @@
Subst
defines a theory of substitution and unification.
+TLA
+Lamport's Temporal Logic of Actions
+
Tools
holds code used to provide support for records, datatypes, induction, etc.
UNITY
Chandy and Misra's UNITY formalism.
+
+W0
+a precursor of MiniML, without let-expressions
Useful references on Higher-Order Logic: