| changeset 12338 | de0f4a63baa5 |
| parent 11190 | 44e157622cb2 |
| child 13792 | d1811693899c |
| 12337:7c6a970f0808 | 12338:de0f4a63baa5 |
|---|---|
14 *) |
14 *) |
15 |
15 |
16 Comp = Union + |
16 Comp = Union + |
17 |
17 |
18 instance |
18 instance |
19 program :: (term)ord |
19 program :: (type) ord |
20 |
20 |
21 defs |
21 defs |
22 component_def "F <= H == EX G. F Join G = H" |
22 component_def "F <= H == EX G. F Join G = H" |
23 strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)" |
23 strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)" |
24 |
24 |