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 theory AC_Equiv imports Main begin (*obviously not Main_ZFC*) |
15 theory AC_Equiv |
|
16 imports Main |
|
17 begin (*obviously not Main_ZFC*) |
16 |
18 |
17 (* Well Ordering Theorems *) |
19 (* Well Ordering Theorems *) |
18 |
20 |
19 definition |
21 definition |
20 "WO1 == \<forall>A. \<exists>R. well_ord(A,R)" |
22 "WO1 == \<forall>A. \<exists>R. well_ord(A,R)" |