author  paulson 
Wed, 08 Sep 1999 15:38:54 +0200  
changeset 7515  0c05469cad57 
parent 4648  f04da668581c 
child 10065  ddb3a014f721 
permissions  rwrr 
7515  1 
(* Title: HOL/Vimage 
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 

4648  9 
Vimage = Set + 
10 

11 
consts 

12 
"``" :: ['a => 'b, 'b set] => ('a set) (infixr 90) 

13 

14 
defs 

15 
vimage_def "f``B == {x. f(x) : B}" 

16 

17 
end 