src/HOL/Inverse_Image.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10832 e33b47e4246d
permissions -rw-r--r--
improved theory reference in comment
     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