changeset 27487 | c8a6ce181805 |
parent 27368 | 9f90ac19e32b |
child 30663 | 0b6aff7451b2 |
27486:c61507a98bff | 27487:c8a6ce181805 |
---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Continuity and iterations (of set transformers) *} |
6 header {* Continuity and iterations (of set transformers) *} |
7 |
7 |
8 theory Continuity |
8 theory Continuity |
9 imports Plain Relation_Power |
9 imports Plain "~~/src/HOL/Relation_Power" |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Continuity for complete lattices *} |
12 subsection {* Continuity for complete lattices *} |
13 |
13 |
14 definition |
14 definition |