| changeset 1203 | a39bec971684 |
| parent 1196 | d43c1f7a53fe |
| child 1401 | 0c439768f45c |
| 1202:968cd786a748 | 1203:a39bec971684 |
|---|---|
1 (* Title: ZF/AC/HH.thy |
1 (* Title: ZF/AC/HH.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Gr`abczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 The theory file for the proofs of |
5 The theory file for the proofs of |
6 AC17 ==> AC1 |
6 AC17 ==> AC1 |
7 AC1 ==> WO2 |
7 AC1 ==> WO2 |
8 AC15 ==> WO6 |
8 AC15 ==> WO6 |