src/FOL/README.html
changeset 3279 815ef5848324
parent 1331 70ee8d7b2233
child 11849 53e629437bc8
--- a/src/FOL/README.html	Wed May 21 17:11:46 1997 +0200
+++ b/src/FOL/README.html	Wed May 21 17:13:00 1997 +0200
@@ -1,27 +1,19 @@
-<HTML><HEAD><TITLE>FOL/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>FOL/README</TITLE></HEAD><BODY>
 
 <H2>FOL: First-Order Logic with Natural Deduction</H2>
 
-This directory contains the Standard ML sources of the Isabelle system for
-First-Order Logic (constructive and classical versions).  For a classical
-sequent calculus, see LK.  Important files include
+This directory contains the ML sources of the Isabelle system for
+First-Order Logic (constructive and classical versions).  For a
+classical sequent calculus, see LK.<p>
 
-<DL>
-<DT>ROOT.ML
-<DD>loads all source files.  Enter an ML image containing Pure
-Isabelle and type: use "ROOT.ML";<P>
-
-<DT>Makefile
-<DD>compiles the files under Poly/ML or SML of New Jersey<P>
-
-<DT>ex
-<DD>subdirectory containing examples.  To execute them, enter an ML image
-containing FOL and type: use "ex/ROOT.ML";<P>
-</DL>
+The <tt>ex</tt> subdirectory contains some examples.<p>
 
 Useful references on First-Order Logic:
 
 <UL>
+<LI> Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991)<br>
+ (The first chapter is an excellent introduction to natural
+deduction in general.)
 <LI>Antony Galton, Logic for Information Technology (Wiley, 1990)
 <LI>Michael Dummett, Elements of Intuitionism (Oxford, 1977)
 </UL>