changeset 1478 | 2b8c2a7547ab |
parent 1401 | 0c439768f45c |
child 11317 | 7f9e4c389318 |
1477:4c51ab632cda | 1478:2b8c2a7547ab |
---|---|
1 (* Title: ZF/AC/AC18_AC19.thy |
1 (* Title: ZF/AC/AC18_AC19.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 Additional definition used in the proof AC19 ==> AC1 which is a part |
5 Additional definition used in the proof AC19 ==> AC1 which is a part |
6 of the chain AC1 ==> AC18 ==> AC19 ==> AC1 |
6 of the chain AC1 ==> AC18 ==> AC19 ==> AC1 |
7 *) |
7 *) |
8 |
8 |