isabelle: src/HOL/Vimage.thy@39ffdb8cab03 (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
f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	11	consts
f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	12	"-``" :: ['a => 'b, 'b set] => ('a set) (infixr 90)
f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	13
f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	14	defs
f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	15	vimage_def "f-``B == {x. f(x) : B}"
f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	16
f04da668581c New theory of the inverse image of a function paulson parents: diff changeset	17	end

author	wenzelm
	Sat, 02 Sep 2000 21:56:24 +0200
changeset 9811	39ffdb8cab03
parent 7515	0c05469cad57
child 10065	ddb3a014f721
permissions	-rw-r--r--