theory file NatSum.thy no longer needed
new files for the Allocator: AllocBase.{thy,ML}
(* 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 +
consts
"-``" :: ['a => 'b, 'b set] => ('a set) (infixr 90)
defs
vimage_def "f-``B == {x. f(x) : B}"
end