changeset 32960 | 69916a850301 |
parent 27678 | 85ea2be46c71 |
child 41777 | 1f7cbe39d425 |
32959:23a8c5ac35f8 | 32960:69916a850301 |
---|---|
1 (* Title: ZF/AC/AC1_AC17.thy |
1 (* Title: ZF/AC/AC1_AC17.thy |
2 ID: $Id$ |
|
3 Author: Krzysztof Grabczewski |
2 Author: Krzysztof Grabczewski |
4 |
3 |
5 The equivalence of AC0, AC1 and AC17 |
4 The equivalence of AC0, AC1 and AC17 |
6 |
5 |
7 Also, the proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent |
6 Also, the proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent |