src/HOL/Inverse_Image.thy
author wenzelm
Sat, 03 Nov 2001 18:42:38 +0100 (2001-11-03)
changeset 12038 343a9888e875
parent 10832 e33b47e4246d
permissions -rw-r--r--
proper use of bind_thm(s);
(*  Title:      HOL/Inverse_Image.thy
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Inverse image of a function
*)

Inverse_Image = Set +

constdefs
  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-`" 90)
    "f-`B  == {x. f(x) : B}"

end