| changeset 16417 | 9bc16273c2d4 |
| parent 14159 | e2eba24c8a2a |
| child 35416 | d8d7d1b785af |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 header{*Examples of Reasoning in ZF Set Theory*} |
1 header{*Examples of Reasoning in ZF Set Theory*} |
2 |
2 |
3 theory ZF_examples = Main_ZFC: |
3 theory ZF_examples imports Main_ZFC begin |
4 |
4 |
5 subsection {* Binary Trees *} |
5 subsection {* Binary Trees *} |
6 |
6 |
7 consts |
7 consts |
8 bt :: "i => i" |
8 bt :: "i => i" |