| changeset 16417 | 9bc16273c2d4 |
| parent 15481 | fc075ae929e4 |
| child 17782 | b3846df9d643 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header{*Zermelo-Fraenkel Set Theory*} |
7 header{*Zermelo-Fraenkel Set Theory*} |
8 |
8 |
9 theory ZF = FOL: |
9 theory ZF imports FOL begin |
10 |
10 |
11 global |
11 global |
12 |
12 |
13 typedecl i |
13 typedecl i |
14 arities i :: "term" |
14 arities i :: "term" |