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
ROOT.ML -- loads all source files. Enter an ML image containing FOL and
type: use "ROOT.ML";
Makefile -- compiles the files under Poly/ML or SML of New Jersey
ex -- subdirectory containing examples. To execute them, enter an ML image
containing ZF and type: use "ex/ROOT.ML";
Useful references on ZF set theory:
Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
Keith J. Devlin,
Fundamentals of Contemporary Set Theory (Springer, 1979)