| changeset 8122 | b43ad07660b9 |
| parent 8055 | bb15396278fb |
| child 8128 | 3a5864b465e2 |
| 8121:4a53041acb28 | 8122:b43ad07660b9 |
|---|---|
24 "preserves v == INT z. stable {s. v s = z}" |
24 "preserves v == INT z. stable {s. v s = z}" |
25 |
25 |
26 funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" |
26 funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" |
27 "funPair f g == %x. (f x, g x)" |
27 "funPair f g == %x. (f x, g x)" |
28 |
28 |
29 (*the set of all sets determined by f alone*) |
|
30 givenBy :: "['a => 'b] => 'a set set" |
|
31 "givenBy f == range (%B. f-`` B)" |
|
32 |
|
29 end |
33 end |