| changeset 578 | efc648d29dd0 |
| parent 516 | 1957113f0d7d |
| child 753 | ec86863e87c8 |
| 577:776b5ba748d8 | 578:efc648d29dd0 |
|---|---|
9 Classical Theorems of Set Theory. |
9 Classical Theorems of Set Theory. |
10 |
10 |
11 Union_in_Pow is proved in ZF.ML |
11 Union_in_Pow is proved in ZF.ML |
12 *) |
12 *) |
13 |
13 |
14 Zorn = OrderArith + AC + "inductive" + |
14 Zorn = OrderArith + AC + "Inductive" + |
15 |
15 |
16 consts |
16 consts |
17 Subset_rel :: "i=>i" |
17 Subset_rel :: "i=>i" |
18 increasing :: "i=>i" |
18 increasing :: "i=>i" |
19 chain, maxchain :: "i=>i" |
19 chain, maxchain :: "i=>i" |