changeset 36452 | d37c6eed8117 |
parent 35918 | 68397d86d454 |
child 39974 | b525988432e9 |
36451:ddc965e172c4 | 36452:d37c6eed8117 |
---|---|
6 |
6 |
7 theory Powerdomain_ex |
7 theory Powerdomain_ex |
8 imports HOLCF |
8 imports HOLCF |
9 begin |
9 begin |
10 |
10 |
11 defaultsort bifinite |
11 default_sort bifinite |
12 |
12 |
13 subsection {* Monadic sorting example *} |
13 subsection {* Monadic sorting example *} |
14 |
14 |
15 domain ordering = LT | EQ | GT |
15 domain ordering = LT | EQ | GT |
16 |
16 |