| changeset 25750 | 4e796867ccb5 |
| parent 23894 | 1a4167d761ac |
| child 26056 | 6a0801279f4c |
| 25749:10e7feb4e595 | 25750:4e796867ccb5 |
|---|---|
6 Zermelo-Fraenkel Set Theory on top of classical First-Order Logic. |
6 Zermelo-Fraenkel Set Theory on top of classical First-Order Logic. |
7 This theory is the work of Martin Coen, Philippe Noel and Lawrence |
7 This theory is the work of Martin Coen, Philippe Noel and Lawrence |
8 Paulson. |
8 Paulson. |
9 *) |
9 *) |
10 |
10 |
11 val banner = "ZF Set Theory (in FOL)"; |
11 use_thy "Main_ZFC"; |
12 writeln banner; |
|
13 |
12 |
14 use_thy "Main_ZFC"; |