isabelle: src/HOL/Vimage.thy@33fe2d701ddd (annotated)

7515 0c05469cad57 comments paulson parents: 4648 diff changeset	1	(* Title: HOL/Vimage
0c05469cad57 comments paulson parents: 4648 diff changeset	2	ID: $Id$
0c05469cad57 comments paulson parents: 4648 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0c05469cad57 comments paulson parents: 4648 diff changeset	4	Copyright 1998 University of Cambridge
0c05469cad57 comments paulson parents: 4648 diff changeset	5
0c05469cad57 comments paulson parents: 4648 diff changeset	6	Inverse image of a function
0c05469cad57 comments paulson parents: 4648 diff changeset	7	*)
0c05469cad57 comments paulson parents: 4648 diff changeset	8
4648 f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	9	Vimage = Set +
f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	10
10065 ddb3a014f721 renaming the inverse image operator in HOL paulson parents: 7515 diff changeset	11	constdefs
ddb3a014f721 renaming the inverse image operator in HOL paulson parents: 7515 diff changeset	12	vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-``" 90)
ddb3a014f721 renaming the inverse image operator in HOL paulson parents: 7515 diff changeset	13	"f-``B == {x. f(x) : B}"
4648 f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	14
f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	15	end