author | lcp |
Thu, 18 May 1995 11:51:23 +0200 | |
changeset 1123 | 5dfdc1464966 |
child 1203 | a39bec971684 |
permissions | -rw-r--r-- |
1123 | 1 |
(* Title: ZF/AC/AC18_AC19.thy |
2 |
ID: $Id$ |
|
3 |
Author: Krzysztof Gr`abczewski |
|
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 |
|
12 |
u_ :: "i => i" |
|
13 |
||
14 |
defs |
|
15 |
||
16 |
u_def "u_(a) == {c Un {0}. c:a}" |
|
17 |
||
18 |
end |