src/HOL/Vimage.thy
changeset 4648 f04da668581c
child 7515 0c05469cad57
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Vimage.thy	Tue Feb 24 11:35:33 1998 +0100
     1.3 @@ -0,0 +1,9 @@
     1.4 +Vimage = Set +
     1.5 +
     1.6 +consts
     1.7 +  "-``"          :: ['a => 'b, 'b set] => ('a set)   (infixr 90)
     1.8 +
     1.9 +defs
    1.10 +  vimage_def     "f-``B           == {x. f(x) : B}"
    1.11 +
    1.12 +end