src/HOL/Vimage.thy
1998-02-24 paulson 1998-02-24 New theory of the inverse image of a function