src/HOL/Set.thy
changeset 35416 d8d7d1b785af
parent 35115 446c5063e4fd
child 35576 5f6bd3ac99f9
     1.1 --- a/src/HOL/Set.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -1586,8 +1586,7 @@
     1.4  
     1.5  subsubsection {* Inverse image of a function *}
     1.6  
     1.7 -constdefs
     1.8 -  vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
     1.9 +definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) where
    1.10    [code del]: "f -` B == {x. f x : B}"
    1.11  
    1.12  lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"