equal
deleted
inserted
replaced
6 AC17 ==> AC1 |
6 AC17 ==> AC1 |
7 AC1 ==> WO2 |
7 AC1 ==> WO2 |
8 AC15 ==> WO6 |
8 AC15 ==> WO6 |
9 *) |
9 *) |
10 |
10 |
11 theory HH imports AC_Equiv Hartog begin |
11 theory HH |
|
12 imports AC_Equiv Hartog |
|
13 begin |
12 |
14 |
13 definition |
15 definition |
14 HH :: "[i, i, i] => i" where |
16 HH :: "[i, i, i] => i" where |
15 "HH(f,x,a) == transrec(a, %b r. let z = x - (\<Union>c \<in> b. r`c) |
17 "HH(f,x,a) == transrec(a, %b r. let z = x - (\<Union>c \<in> b. r`c) |
16 in if f`z \<in> Pow(z)-{0} then f`z else {x})" |
18 in if f`z \<in> Pow(z)-{0} then f`z else {x})" |