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