changeset 12338 | de0f4a63baa5 |
parent 12030 | 46d57d0290a2 |
child 14981 | e73f8140af78 |
12337:7c6a970f0808 | 12338:de0f4a63baa5 |
---|---|
6 Discrete CPOs. |
6 Discrete CPOs. |
7 *) |
7 *) |
8 |
8 |
9 Discrete = Discrete1 + |
9 Discrete = Discrete1 + |
10 |
10 |
11 instance discr :: (term)cpo (discr_cpo) |
11 instance discr :: (type)cpo (discr_cpo) |
12 |
12 |
13 constdefs |
13 constdefs |
14 undiscr :: ('a::term)discr => 'a |
14 undiscr :: ('a::type)discr => 'a |
15 "undiscr x == (case x of Discr y => y)" |
15 "undiscr x == (case x of Discr y => y)" |
16 |
16 |
17 end |
17 end |