| changeset 10065 | ddb3a014f721 |
| parent 7515 | 0c05469cad57 |
| 10064:1a77667b21ef | 10065:ddb3a014f721 |
|---|---|
6 Inverse image of a function |
6 Inverse image of a function |
7 *) |
7 *) |
8 |
8 |
9 Vimage = Set + |
9 Vimage = Set + |
10 |
10 |
11 consts |
11 constdefs |
12 "-``" :: ['a => 'b, 'b set] => ('a set) (infixr 90) |
12 vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-``" 90) |
13 |
13 "f-``B == {x. f(x) : B}" |
14 defs |
|
15 vimage_def "f-``B == {x. f(x) : B}" |
|
16 |
14 |
17 end |
15 end |