| changeset 48462 | 424fd5364f15 |
| parent 46972 | ef6fc1a0884d |
| child 48733 | 18e76e2db6d4 |
| 48461:96c1ef26aabe | 48462:424fd5364f15 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header{*Zermelo-Fraenkel Set Theory*} |
6 header{*Zermelo-Fraenkel Set Theory*} |
7 |
7 |
8 theory ZF |
8 theory ZF |
9 imports FOL |
9 imports "~~/src/FOL/FOL" |
10 begin |
10 begin |
11 |
11 |
12 declare [[eta_contract = false]] |
12 declare [[eta_contract = false]] |
13 |
13 |
14 typedecl i |
14 typedecl i |