equal
deleted
inserted
replaced
18 So we don't have to prove all implications of both cases. |
18 So we don't have to prove all implications of both cases. |
19 Moreover we don't need to prove AC13(1) ==> AC1 and AC11 ==> AC14 as |
19 Moreover we don't need to prove AC13(1) ==> AC1 and AC11 ==> AC14 as |
20 Rubin & Rubin do. |
20 Rubin & Rubin do. |
21 *) |
21 *) |
22 |
22 |
23 theory AC15_WO6 imports HH Cardinal_aux begin |
23 theory AC15_WO6 |
|
24 imports HH Cardinal_aux |
|
25 begin |
24 |
26 |
25 |
27 |
26 (* ********************************************************************** *) |
28 (* ********************************************************************** *) |
27 (* Lemmas used in the proofs in which the conclusion is AC13, AC14 *) |
29 (* Lemmas used in the proofs in which the conclusion is AC13, AC14 *) |
28 (* or AC15 *) |
30 (* or AC15 *) |