changeset 12257 | e3f7d6fb55d7 |
parent 12256 | 26243ebf2831 |
child 12258 | 5da24e7e9aba |
12256:26243ebf2831 | 12257:e3f7d6fb55d7 |
---|---|
1 (* Title: HOL/Inverse_Image.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Inverse image of a function |
|
7 *) |
|
8 |
|
9 Inverse_Image = Set + |
|
10 |
|
11 constdefs |
|
12 vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-`" 90) |
|
13 "f-`B == {x. f(x) : B}" |
|
14 |
|
15 end |