| changeset 35939 | db69a6a1fbb5 |
| parent 35932 | 86559356502d |
| child 36075 | 2e0370c03066 |
| 35938:93faaa15c3d5 | 35939:db69a6a1fbb5 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Fixed point operator and admissibility *} |
6 header {* Fixed point operator and admissibility *} |
7 |
7 |
8 theory Fix |
8 theory Fix |
9 imports Cfun Cprod |
9 imports Cfun |
10 begin |
10 begin |
11 |
11 |
12 defaultsort pcpo |
12 defaultsort pcpo |
13 |
13 |
14 subsection {* Iteration *} |
14 subsection {* Iteration *} |