diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Inverse_Image.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Inverse_Image.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,15 @@
+(*  Title:      HOL/Inverse_Image.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Inverse image of a function
+*)
+
+Inverse_Image = Set +
+
+constdefs
+  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-``" 90)
+    "f-``B  == {x. f(x) : B}"
+
+end