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
nipkow@10213
     1
(*  Title:      HOL/Inverse_Image.thy
nipkow@10213
     2
    ID:         $Id$
nipkow@10213
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
nipkow@10213
     4
    Copyright   1998  University of Cambridge
nipkow@10213
     5
nipkow@10213
     6
Inverse image of a function
nipkow@10213
     7
*)
nipkow@10213
     8
nipkow@10213
     9
Inverse_Image = Set +
nipkow@10213
    10
nipkow@10213
    11
constdefs
nipkow@10832
    12
  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-`" 90)
nipkow@10832
    13
    "f-`B  == {x. f(x) : B}"
nipkow@10213
    14
nipkow@10213
    15
end