src/HOL/Vimage.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7515 0c05469cad57
child 10065 ddb3a014f721
permissions -rw-r--r--
tidied; added lemma restrict_to_left
paulson@7515
     1
(*  Title:      HOL/Vimage
paulson@7515
     2
    ID:         $Id$
paulson@7515
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7515
     4
    Copyright   1998  University of Cambridge
paulson@7515
     5
paulson@7515
     6
Inverse image of a function
paulson@7515
     7
*)
paulson@7515
     8
paulson@4648
     9
Vimage = Set +
paulson@4648
    10
paulson@4648
    11
consts
paulson@4648
    12
  "-``"          :: ['a => 'b, 'b set] => ('a set)   (infixr 90)
paulson@4648
    13
paulson@4648
    14
defs
paulson@4648
    15
  vimage_def     "f-``B           == {x. f(x) : B}"
paulson@4648
    16
paulson@4648
    17
end