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