--- a/src/LCF/README.html Wed May 21 17:11:46 1997 +0200
+++ b/src/LCF/README.html Wed May 21 17:13:00 1997 +0200
@@ -1,24 +1,13 @@
-<HTML><HEAD><TITLE>LCF/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>LCF/README</TITLE></HEAD><BODY>
<H2>LCF: Logic for Computable Functions</H2>
-This directory contains the Standard ML sources of the Isabelle system for
-LCF. It is loaded upon FOL, not Pure Isabelle. Important files include
-
-<DL>
-<DT>ROOT.ML
-<DD>loads all source files. Enter an ML image containing FOL
-Isabelle and type: use "ROOT.ML";<P>
+This directory contains the ML sources of the Isabelle system for
+LCF, based on FOL.<p>
-<DT>Makefile
-<DD>compiles the files under Poly/ML or SML of New Jersey<P>
+The <tt>ex</tt> subdirectory contains some examples.<p>
-<DT>ex.ML
-<DD>file containing examples. To execute it, enter an ML image
-containing LCF and type: use "ex.ML";
-</DL>
-
-Useful references on First-Order Logic:
+Useful references on LCF:
<UL>
<LI>Lawrence C. Paulson,<BR>