| changeset 26852 | a31203f58b20 |
| parent 26845 | d86eb226ecba |
| child 26894 | 1120f6cc10b0 |
| 26851:0242c9c980df | 26852:a31203f58b20 |
|---|---|
2 |
2 |
3 theory ZF_Specific |
3 theory ZF_Specific |
4 imports ZF |
4 imports ZF |
5 begin |
5 begin |
6 |
6 |
7 chapter {* ZF specific elements *} |
7 chapter {* Isabelle/ZF \label{ch:zf} *} |
8 |
8 |
9 section {* Type checking *} |
9 section {* Type checking *} |
10 |
10 |
11 text {* |
11 text {* |
12 The ZF logic is essentially untyped, so the concept of ``type |
12 The ZF logic is essentially untyped, so the concept of ``type |