--- a/src/HOL/README.html Thu Aug 19 16:33:53 1999 +0200
+++ b/src/HOL/README.html Thu Aug 19 16:54:38 1999 +0200
@@ -20,8 +20,9 @@
<DT>Induct
<DD>examples of (co)inductive definitions
-<DT>Integ
-<DD>a theory of the integers including efficient integer calculations
+<DT>Integ
+<DD>a development of the integers including efficient integer
+calculations (part of the standard HOL environment)
<DT>IOA
<DD>extended example of Input/Output Automata
@@ -29,8 +30,19 @@
<DT>Lambda
<DD>a proof of the Church-Rosser theorem for lambda-calculus
+<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
+the image HOL-Real.
+
<DT>Subst
-<DD>subdirectory defining a theory of substitution and unification.
+<DD>defines a theory of substitution and unification.
+
+<DT>Tools
+<DD>holds code used to provide support for records, datatypes, induction, etc.
+
+<DT>UNITY
+<DD>Chandy and Misra's UNITY formalism.
</DL>
Useful references on Higher-Order Logic: