0
|
1 |
ZF: Zermelo-Fraenkel 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)
|