| changeset 21326 | c33cdc5a6c7c |
| parent 21316 | 4d913b8bccf1 |
| child 21404 | eb85850d3eb7 |
| 21325:df6392bda693 | 21326:c33cdc5a6c7c |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header{* Fixed Points and the Knaster-Tarski Theorem*} |
8 header{* Fixed Points and the Knaster-Tarski Theorem*} |
9 |
9 |
10 theory FixedPoint |
10 theory FixedPoint |
11 imports Product_Type |
11 imports Product_Type LOrder |
12 begin |
12 begin |
13 |
13 |
14 subsection {* Complete lattices *} |
14 subsection {* Complete lattices *} |
15 (*FIXME Meet \<rightarrow> Inf *) |
15 (*FIXME Meet \<rightarrow> Inf *) |
16 consts |
16 consts |