| changeset 58889 | 5b7a9633cfa8 |
| parent 58860 | fee7cfa69c50 |
| child 65449 | c82e63b11b8b |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
1 header{*Examples of Reasoning in ZF Set Theory*} |
1 section{*Examples of Reasoning in ZF Set Theory*} |
2 |
2 |
3 theory ZF_examples imports Main_ZFC begin |
3 theory ZF_examples imports Main_ZFC begin |
4 |
4 |
5 subsection {* Binary Trees *} |
5 subsection {* Binary Trees *} |
6 |
6 |