src/HOL/Vimage.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Vimage.thy	Tue Feb 24 11:35:33 1998 +0100
@@ -0,0 +1,9 @@
+Vimage = Set +
+
+consts
+  "-``"          :: ['a => 'b, 'b set] => ('a set)   (infixr 90)
+
+defs
+  vimage_def     "f-``B           == {x. f(x) : B}"
+
+end