author | paulson |
Thu, 12 Apr 2001 12:45:05 +0200 | |
changeset 11251 | a6816d47f41d |
parent 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 |
|
10832 | 12 |
vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-`" 90) |
13 |
"f-`B == {x. f(x) : B}" |
|
10213 | 14 |
|
15 |
end |