isabelle: src/HOL/Inverse_Image.thy@28a53b68a8c0 (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
10832 e33b47e4246d `` -> and ``` -> `` nipkow parents: 10213 diff changeset	12	vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-`" 90)
e33b47e4246d `` -> and ``` -> `` nipkow parents: 10213 diff changeset	13	"f-`B == {x. f(x) : B}"
10213 01c2744a3786 * empty log message * nipkow parents: diff changeset	14
01c2744a3786 * empty log message * nipkow parents: diff changeset	15	end