--- a/src/ZF/README.html Wed May 21 17:11:46 1997 +0200
+++ b/src/ZF/README.html Wed May 21 17:13:00 1997 +0200
@@ -1,25 +1,11 @@
-<HTML><HEAD><TITLE>ZF/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY>
<H2>ZF: Zermelo-Fraenkel Set Theory</H2>
-This directory contains the Standard ML sources of the Isabelle system for
-ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files
-include
-
-<DL>
-<DT>Makefile
-<DD>compiles the files under Poly/ML or SML of New Jersey. Can also
-run all the tests described below.<P>
+This directory contains the ML sources of the Isabelle system for
+ZF Set Theory, based on FOL.<p>
-<DT>ROOT.ML
-<DD>loads all source files. Enter an ML image containing FOL and
-type: use "ROOT.ML";
-</DL>
-
-There are also several subdirectories of examples. To execute the examples on
-some directory <Dir>, enter an ML image containing ZF and type
-<TT>use "<Dir>/ROOT.ML";</TT>
-
+There are several subdirectories of examples:
<DL>
<DT>AC
<DD>subdirectory containing proofs from the book "Equivalents of the Axiom