--- a/src/HOL/README.html Thu Feb 12 14:53:00 1998 +0100
+++ b/src/HOL/README.html Thu Feb 12 15:00:04 1998 +0100
@@ -36,12 +36,29 @@
Useful references on Higher-Order Logic:
<UL>
-<LI>P. B. Andrews,<BR>
+
+<LI> P. B. Andrews,<BR>
An Introduction to Mathematical Logic and Type Theory<BR>
(Academic Press, 1986).
-<LI>J. Lambek and P. J. Scott,<BR>
- Introduction to Higher Order Categorical Logic (CUP, 1986)
+<P>
+
+<LI> A. Church,<BR>
+ A Formulation of the Simple Theory of Types<BR>
+ (Journal of Symbolic Logic, 1940).
+
+<P>
+
+<LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
+ Introduction to HOL: A theorem proving environment for higher order logic<BR>
+ (Cambridge University Press, 1993).
+
+<P>
+
+<LI> J. Lambek and P. J. Scott,<BR>
+ Introduction to Higher Order Categorical Logic<BR>
+ (Cambridge University Press, 1986).
+
</UL>
</BODY></HTML>