equal
deleted
inserted
replaced
1 <HTML><HEAD><TITLE>ZF/ReadMe</TITLE></HEAD><BODY> |
1 <HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY> |
2 |
2 |
3 <H2>ZF: Zermelo-Fraenkel Set Theory</H2> |
3 <H2>ZF: Zermelo-Fraenkel Set Theory</H2> |
4 |
4 |
5 This directory contains the Standard ML sources of the Isabelle system for |
5 This directory contains the ML sources of the Isabelle system for |
6 ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files |
6 ZF Set Theory, based on FOL.<p> |
7 include |
|
8 |
7 |
9 <DL> |
8 There are several subdirectories of examples: |
10 <DT>Makefile |
|
11 <DD>compiles the files under Poly/ML or SML of New Jersey. Can also |
|
12 run all the tests described below.<P> |
|
13 |
|
14 <DT>ROOT.ML |
|
15 <DD>loads all source files. Enter an ML image containing FOL and |
|
16 type: use "ROOT.ML"; |
|
17 </DL> |
|
18 |
|
19 There are also several subdirectories of examples. To execute the examples on |
|
20 some directory <Dir>, enter an ML image containing ZF and type |
|
21 <TT>use "<Dir>/ROOT.ML";</TT> |
|
22 |
|
23 <DL> |
9 <DL> |
24 <DT>AC |
10 <DT>AC |
25 <DD>subdirectory containing proofs from the book "Equivalents of the Axiom |
11 <DD>subdirectory containing proofs from the book "Equivalents of the Axiom |
26 of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof |
12 of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof |
27 Gr`abczewski.<P> |
13 Gr`abczewski.<P> |