isabelle: src/HOL/Vimage.thy@efbe50e2bef9 (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	paulson
	Fri, 07 Jan 2000 11:00:56 +0100
changeset 8112	efbe50e2bef9
parent 7515	0c05469cad57
child 10065	ddb3a014f721
permissions	-rw-r--r--