| changeset 10832 | e33b47e4246d |
| parent 10213 | 01c2744a3786 |
| 10831:024bdf8e52a4 | 10832:e33b47e4246d |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 Inverse_Image = Set + |
9 Inverse_Image = Set + |
10 |
10 |
11 constdefs |
11 constdefs |
12 vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-``" 90) |
12 vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-`" 90) |
13 "f-``B == {x. f(x) : B}" |
13 "f-`B == {x. f(x) : B}" |
14 |
14 |
15 end |
15 end |