changeset 16082 | ebb53ebfd4e2 |
parent 16079 | 757e1c4a8081 |
child 16214 | e3816a7db016 |
16081:81a4b4a245b0 | 16082:ebb53ebfd4e2 |
---|---|
8 header {* Fixed point operator and admissibility *} |
8 header {* Fixed point operator and admissibility *} |
9 |
9 |
10 theory Fix |
10 theory Fix |
11 imports Cfun Cprod Adm |
11 imports Cfun Cprod Adm |
12 begin |
12 begin |
13 |
|
14 defaultsort pcpo |
|
13 |
15 |
14 subsection {* Definitions *} |
16 subsection {* Definitions *} |
15 |
17 |
16 consts |
18 consts |
17 |
19 |