src/HOL/README.html
changeset 15916 1314ef1e49dd
parent 15910 5df57194d064
child 31795 be3e1cc5005c
equal deleted inserted replaced
15915:b0e8b37642a4 15916:1314ef1e49dd
   117 <dt>ex
   117 <dt>ex
   118 <dd>miscellaneous examples
   118 <dd>miscellaneous examples
   119 
   119 
   120 </dl>
   120 </dl>
   121 
   121 
   122 Useful references on Higher-Order Logic:
       
   123 
       
   124 <ul>
       
   125 
       
   126 <li>P. B. Andrews,<br>
       
   127 An Introduction to Mathematical Logic and Type Theory<br>
       
   128 (Academic Press, 1986).
       
   129 
       
   130 <li>A. Church,<br>
       
   131 A Formulation of the Simple Theory of Types<br>
       
   132 (Journal of Symbolic Logic, 1940).
       
   133 
       
   134 <li>M. J. C. Gordon and T. F. Melham (editors),<br>
       
   135 Introduction to HOL: A theorem proving environment for higher order logic<br>
       
   136 (Cambridge University Press, 1993).
       
   137 
       
   138 <li>J. Lambek and P. J. Scott,<br>
       
   139 Introduction to Higher Order Categorical Logic<br>
       
   140 (Cambridge University Press, 1986).
       
   141 
       
   142 </ul>
       
   143 
       
   144 </body>
   122 </body>
   145 </html>
   123 </html>