author | wenzelm |
Sun, 15 Oct 2000 19:50:35 +0200 | |
changeset 10220 | 2a726de6e124 |
parent 1478 | 2b8c2a7547ab |
child 11317 | 7f9e4c389318 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/AC/AC18_AC19.thy |
1123 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Krzysztof Grabczewski |
1123 | 4 |
|
5 |
Additional definition used in the proof AC19 ==> AC1 which is a part |
|
6 |
of the chain AC1 ==> AC18 ==> AC19 ==> AC1 |
|
7 |
*) |
|
8 |
||
9 |
AC18_AC19 = AC_Equiv + |
|
10 |
||
11 |
consts |
|
1401 | 12 |
u_ :: i => i |
1123 | 13 |
|
14 |
defs |
|
15 |
||
16 |
u_def "u_(a) == {c Un {0}. c:a}" |
|
17 |
||
1203 | 18 |
end |