changeset 12338 | de0f4a63baa5 |
parent 12030 | 46d57d0290a2 |
child 14981 | e73f8140af78 |
12337:7c6a970f0808 | 12338:de0f4a63baa5 |
---|---|
6 Discrete CPOs. |
6 Discrete CPOs. |
7 *) |
7 *) |
8 |
8 |
9 Discrete0 = Cont + Datatype + |
9 Discrete0 = Cont + Datatype + |
10 |
10 |
11 datatype 'a discr = Discr "'a :: term" |
11 datatype 'a discr = Discr "'a :: type" |
12 |
12 |
13 instance discr :: (term)sq_ord |
13 instance discr :: (type) sq_ord |
14 |
14 |
15 defs |
15 defs |
16 less_discr_def "((op <<)::('a::term)discr=>'a discr=>bool) == op =" |
16 less_discr_def "((op <<)::('a::type)discr=>'a discr=>bool) == op =" |
17 |
17 |
18 end |
18 end |