# HG changeset patch
# User wenzelm
# Date 887292004 -3600
# Node ID 85aae356570c7eea90068829d117e7761f7fff1a
# Parent  79e6a11ba8a992af01ddacb040ef47e1c2c6716d
tuned;

diff -r 79e6a11ba8a9 -r 85aae356570c src/HOL/README.html
--- 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>