src/HOL/Inverse_Image.thy
changeset 10213 01c2744a3786
child 10832 e33b47e4246d
equal deleted inserted replaced
10212:33fe2d701ddd 10213:01c2744a3786
       
     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