equal
deleted
inserted
replaced
10 Some Isabelle proofs of equivalences of these axioms are formalizations of |
10 Some Isabelle proofs of equivalences of these axioms are formalizations of |
11 proofs presented by the Rubins. The others are based on the Rubins' proofs, |
11 proofs presented by the Rubins. The others are based on the Rubins' proofs, |
12 but slightly changed. |
12 but slightly changed. |
13 *) |
13 *) |
14 |
14 |
15 AC_Equiv = CardinalArith + Univ + OrdQuant + |
15 AC_Equiv = CardinalArith + Univ + |
16 |
16 |
17 consts |
17 consts |
18 |
18 |
19 (* Well Ordering Theorems *) |
19 (* Well Ordering Theorems *) |
20 WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: o |
20 WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: o |