src/HOL/README.html
changeset 4622 85aae356570c
parent 3279 815ef5848324
child 7290 f1a37c379317
     1.1 --- a/src/HOL/README.html	Thu Feb 12 14:53:00 1998 +0100
     1.2 +++ b/src/HOL/README.html	Thu Feb 12 15:00:04 1998 +0100
     1.3 @@ -36,12 +36,29 @@
     1.4  Useful references on Higher-Order Logic:
     1.5  
     1.6  <UL>
     1.7 -<LI>P. B. Andrews,<BR>
     1.8 +
     1.9 +<LI> P. B. Andrews,<BR>
    1.10      An Introduction to Mathematical Logic and Type Theory<BR>
    1.11      (Academic Press, 1986).
    1.12  
    1.13 -<LI>J. Lambek and P. J. Scott,<BR>
    1.14 -    Introduction to Higher Order Categorical Logic (CUP, 1986)
    1.15 +<P>
    1.16 +
    1.17 +<LI> A. Church,<BR>
    1.18 +    A Formulation of the Simple Theory of Types<BR>
    1.19 +    (Journal of Symbolic Logic, 1940).
    1.20 +
    1.21 +<P>
    1.22 +
    1.23 +<LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
    1.24 +    Introduction to HOL: A theorem proving environment for higher order logic<BR>
    1.25 +    (Cambridge University Press, 1993).
    1.26 +
    1.27 +<P>
    1.28 +
    1.29 +<LI> J. Lambek and P. J. Scott,<BR>
    1.30 +    Introduction to Higher Order Categorical Logic<BR>
    1.31 +    (Cambridge University Press, 1986).
    1.32 +
    1.33  </UL>
    1.34  
    1.35  </BODY></HTML>