diff -r 636322bfd057 -r 815ef5848324 src/ZF/README.html --- 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 @@ -ZF/ReadMe +ZF/README

ZF: Zermelo-Fraenkel Set Theory

-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 - -
Makefile -
compiles the files under Poly/ML or SML of New Jersey. Can also -run all the tests described below.

+This directory contains the ML sources of the Isabelle system for +ZF Set Theory, based on FOL.


loads all source files. Enter an ML image containing FOL and -type: use "ROOT.ML"; -
- -There are also several subdirectories of examples. To execute the examples on -some directory <Dir>, enter an ML image containing ZF and type -use "<Dir>/ROOT.ML"; - +There are several subdirectories of examples:
subdirectory containing proofs from the book "Equivalents of the Axiom