0

1 
ZF: ZermeloFraenkel Set Theory


2 


3 
This directory contains the Standard ML sources of the Isabelle system for


4 
ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files


5 
include


6 


7 
ROOT.ML  loads all source files. Enter an ML image containing FOL and


8 
type: use "ROOT.ML";


9 


10 
Makefile  compiles the files under Poly/ML or SML of New Jersey


11 


12 
ex  subdirectory containing examples. To execute them, enter an ML image


13 
containing ZF and type: use "ex/ROOT.ML";


14 


15 
Useful references on ZF set theory:


16 


17 
Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)


18 


19 
Patrick Suppes, Axiomatic Set Theory (Dover, 1972)


20 


21 
Keith J. Devlin,


22 
Fundamentals of Contemporary Set Theory (Springer, 1979)
