author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 488 52f7447d4f1b
permissions -rw-r--r--
Initial revision

		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

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)