isabelle: src/HOL/Inverse_Image.thy@d3f780c3af0c (annotated)

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