| author | nipkow |
| Tue, 17 Oct 2000 08:00:46 +0200 | |
| changeset 10228 | e653cb933293 |
| parent 10213 | 01c2744a3786 |
| child 10832 | e33b47e4246d |
| permissions | -rw-r--r-- |
| 10213 | 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 |